proposition: Lemma Qcmult_le_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' Hle Hle'. etransitivity. apply Qcmult_le_compat_l; eassumption. apply Qcmult_le_compat_r. assumption. etransitivity; eassumption. Qed.
imports: Qfield Qreduction Qcanon