proposition: Lemma Qcmult_lt_l : forall q₁ q₂ q₃, 0 < q₃ -> (q₃ * q₁ < q₃ * q₂ <-> q₁ < q₂).
proof: Proof. intros q q₂ q₃. unfold Qclt,Qcmult,Qred. repeat rewrite Q2Qc_correct. apply Qmult_lt_l. Qed.
imports: Qfield Qreduction Qcanon