proposition: Lemma ratSubtract_ratAdd_inverse_2 : forall r1 r2, r2 <= r1 -> r2 + ratSubtract r1 r2 == r1.
proof: Proof. intuition. apply eqRat_symm. eapply eqRat_trans. 2:{ apply ratSubtract_ratAdd_assoc. trivial. } apply eqRat_symm. apply ratSubtract_ratAdd_inverse. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms