proposition: Lemma Qcminus_le_compat : forall q₁ q₂ q₃ q₄, q₁ <= q₃ -> q₄ <= q₂ -> q₁ - q₂ <= q₃ - q₄.
proof: Proof. intros q₁ q₂ q₃ q₄ Hle₁ Hle₂. unfold Qcminus,Qcopp,Qcplus,Qcle. repeat rewrite Q2Qc_correct. apply Qplus_le_compat. easy. now apply Qopp_le_compat. Qed.
imports: Qfield Qreduction Qcanon