Exercise. Rule Induction, Automation, Structured Proofs › Even numbers are multiples of two [isa-002L]

lemma "even n ⟹ ∃m. (m * 2 = n)"