proposition: Lemma leRat_difference_exists : forall r1 r2, r2 <= r1 -> exists r3, r1 == r2 + r3.
proof: Proof. intuition. exists (ratSubtract r1 r2). apply eqRat_symm. apply ratSubtract_ratAdd_inverse_2. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms