proposition: Theorem ratAdd_leRat_compat : forall r1 r2 r3 r4, leRat r1 r2 -> leRat r3 r4 -> r1 + r3 <= r2 + r4.
proof: Proof. intuition. eapply leRat_trans. eapply ratAdd_leRat_compat_l; eauto. rewrite ratAdd_comm. eapply leRat_trans. apply ratAdd_leRat_compat_l; eauto. rewrite ratAdd_comm. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms