proposition: Lemma leRat_ratAdd_same_r : forall r1 r2 r3, r2 + r1 <= r3 + r1 -> r2 <= r3.
proof: Proof. intuition. apply (@ratSubtract_leRat_l (r2 + r1) (r3 + r1) r1) in H. rewrite <- (@ratSubtract_ratAdd_inverse r1 r2). rewrite ratAdd_comm. rewrite H. rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_inverse. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms