proposition: Lemma ratAdd_any_leRat_r : forall r1 r2 r3, r1 <= r2 -> r1 <= r3 + r2.
proof: Proof. intros. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. apply ratAdd_comm. } apply ratAdd_any_leRat_l; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms