proposition: Lemma ratAdd_any_le : forall r1 r2 r3, r1 + r2 <= r3 -> r1 <= r3.
proof: Proof. intuition. eapply leRat_trans. eapply eqRat_impl_leRat. apply ratAdd_0_r. eapply leRat_trans. eapply ratAdd_leRat_compat. apply leRat_refl. apply rat0_le_all. eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms