proposition: Lemma ratAdd_eq_impl_leRat_l : forall r1 r2 r3, r1 == r2 + r3 -> r2 <= r1.
proof: Proof. intuition. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply eqRat_symm. eapply H. } apply ratAdd_any_leRat_l. apply leRat_refl. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms