proposition: Lemma lem_main : forall n m, n * n = 2 * m * m -> m = 0.
proof: Proof. intro n; pattern n; apply lt_wf_ind; clear n. intros n H m H0. destruct (Nat.eq_dec n 0) as [H1|H1]; subst. - sauto. - destruct (even_odd_cor n) as [k HH]. destruct HH as [H2|H2]; subst. + assert (2 * k * k = m * m) by lia. assert (m < 2 * k). { qauto use: @Nat.mul_0_r, @lem_0. } sauto. + sauto. Qed.
imports: Hammer(Tactics) Reals Arith Wf_nat Even Lia