proposition: Lemma ratAdd_add_same_r : forall r1 r2 r3, r1 + r2 == r3 + r2 -> r1 == r3.
proof: Proof. intuition. assert (ratSubtract (r1 + r2) r2 == ratSubtract (r3 + r2) r2). eapply ratSubtract_eqRat_compat; intuition. rewrite ratSubtract_ratAdd_assoc in H0. setoid_rewrite ratAdd_0_r. eapply eqRat_trans. eapply ratAdd_eqRat_compat. eapply eqRat_refl. eapply eqRat_symm. apply (@ratSubtract_0 r2 r2). eapply leRat_refl. rewrite H0. rewrite ratSubtract_ratAdd_assoc. eapply ratAdd_eqRat_compat. intuition. apply ratSubtract_0. eapply leRat_refl. apply leRat_refl. apply leRat_refl. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms