proposition: Lemma Qcplus_lt_le_compat : forall q₁ q₂ q₃ q₄, q₁ < q₃ -> q₂ <= q₄ -> q₁ + q₂ < q₃ + q₄.
proof: Proof. intros q₁ q₂ q₃ q₄ Hlt Hle. unfold Qcplus,Qclt. repeat rewrite Q2Qc_correct. now apply Qplus_lt_le_compat. Qed.
imports: Qfield Qreduction Qcanon