proposition: Lemma lem_0 : forall n m, n <> 0 -> m * m = 2 * n * n -> m < 2 * n.
proof: Proof. intros n m H H0. destruct (lt_dec m (2 * n)) as [|H1]; try strivial. exfalso. assert (m >= 2 * n) by lia. clear H1. assert (m * m >= 2 * n * (2 * n)). { assert (m * m >= 2 * n * m). { hauto use: @Nat.le_0_l, @Nat.mul_le_mono_nonneg_r unfold: ge. } assert (2 * n * m >= 2 * n * (2 * n)). { hauto use: @Nat.le_0_l, @Nat.mul_le_mono_nonneg_l unfold: ge. } eauto with arith. } sauto. Qed.
imports: Hammer(Tactics) Reals Arith Wf_nat Even Lia