proposition: Lemma ratSubtract_leRat : forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> ratSubtract r1 r4 <= ratSubtract r2 r3.
proof: Proof. intuition. eapply leRat_trans. eapply ratSubtract_leRat_l; eauto. eapply ratSubtract_leRat_r; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms