proposition: Lemma ratSubtract_ratAdd_assoc: forall r1 r2 r3, r3 <= r2 -> ratSubtract (r1 + r2) r3 == r1 + (ratSubtract r2 r3).
proof: Proof. intuition. unfold ratSubtract. rattac. arithNormalize. rewrite minus_plus_assoc. f_equal. f_equal. do 5 arithSimplify. do 5 arithSimplify. do 3 (eapply Nat.mul_le_mono; trivial). repeat rewrite <- Nat.mul_assoc. repeat rewrite (Nat.mul_comm x). repeat rewrite Nat.mul_assoc. apply Nat.mul_le_mono; trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms