proposition: Lemma Qcsquare_pos : forall q, q <> 0 -> 0 < q * q.
proof: Proof. intros q Hq. destruct (Qcle_lt_or_eq _ _ (Qcsquare_nonneg q)) as [| Heq]. assumption. symmetry in Heq. apply Qcmult_integral in Heq. destruct Heq; contradiction. Qed.
imports: Qfield Qreduction Qcanon