proposition: Lemma Qcmult_resp_nonneg : forall q q', 0 <= q -> 0 <= q' -> 0 <= q * q'.
proof: Proof. intros q q' Hq Hq'. apply Qcle_trans with (0 * q'). now unfold Qcle,Q2Qc,Qred. now apply Qcmult_le_compat_r. Qed.
imports: Qfield Qreduction Qcanon