proposition: Theorem sqrt2_not_rational : forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.
proof: Proof. intros p q; generalize p; clear p; elim q using (well_founded_ind lt_wf). clear q; intros q Hrec p Hneq; pose proof Hneq as Hlt_O_q; apply Nat.neq_0_lt_0 in Hlt_O_q; intros Heq. apply (Hrec (3 * q - 2 * p) (comparison4 _ _ Hlt_O_q Heq) (3 * p - 4 * q)). apply sym_not_equal; apply lt_neq; apply Nat.add_lt_mono_l with (2 * p); rewrite <- plus_n_O; rewrite Nat.add_comm; rewrite Nat.sub_add; auto with *. apply new_equality; auto. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)