proposition: Theorem sqrt_q_non_zero : 0 <> q * q.
proof: Proof. generalize pos_q; case q. intros H; elim (Nat.nlt_0_r 0); auto. intros n H. simpl in |- *; discriminate. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)