proposition: Lemma ratSubtract_partition : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> (ratSubtract r3 r1) == (ratSubtract r2 r1) + (ratSubtract r3 r2).
proof: Proof. rattac. unfold ratSubtract in *. rattac. arithNormalize. rewrite <- Nat.add_sub_swap. eapply minus_eq_compat. rewrite minus_add_assoc. rewrite Nat.add_comm. rewrite <- minus_add_assoc. rewrite <- Nat.add_0_r at 1. apply plus_eq_compat. do 4 arithSimplify. symmetry. eapply minus_diag_eq. do 4 arithSimplify. apply le_eq. do 5 arithSimplify. do 4 (apply Nat.mul_le_mono; trivial). do 4 arithSimplify. do 4 (apply Nat.mul_le_mono; trivial). Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms