proposition: Lemma Qcmult_lt_r : 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_r. Qed.
imports: Qfield Qreduction Qcanon