proposition: Lemma Qcmult_lt_compat : forall q₁ q₂ q₃ q₄, 0 < q₁ -> 0 < q₃ -> q₁ < q₂ -> q₃ < q₄ -> q₁ * q₃ < q₂ * q₄.
proof: Proof. intros q₁ q₂ q₃ q₄ Hpos Hpos' Hlt Hlt'. apply Qclt_trans with (q₁ * q₄). rewrite Qcmult_lt_l; eassumption. rewrite Qcmult_lt_r. assumption. apply Qclt_trans with q₃; eassumption. Qed.
imports: Qfield Qreduction Qcanon