proposition: Lemma Qcplus_le_lt_compat : forall q₁ q₂ q₃ q₄, q₁ <= q₃ -> q₂ < q₄ -> q₁ + q₂ < q₃ + q₄.
proof: Proof. intros q₁ q₂ q₃ q₄ Hle Hlt. setoid_rewrite Qcplus_comm. now apply Qcplus_lt_le_compat. Qed.
imports: Qfield Qreduction Qcanon