proposition: Lemma Qmult_mult_nonneg: forall x:Q, Zero <= x*x.
proof: Proof. let T_local := apply Qlt_le_weak; apply Qsgn_9; rewrite Qsgn_15; reflexivity in (intros [|x|x]; [ apply Qle_reflexive | T_local | T_local ]). Qed.