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