proposition: Lemma eqRat_ratAdd_same_r : forall r1 r2 r3, r2 + r1 == r3 + r1 -> r2 == r3.
proof: Proof. intuition. eapply leRat_impl_eqRat. eapply leRat_ratAdd_same_r; eapply eqRat_impl_leRat; eauto. symmetry in H. eapply leRat_ratAdd_same_r; eapply eqRat_impl_leRat; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms