proposition: Lemma ratSubtract_eqRat_compat : forall r1 r2 r3 r4, r1 == r3 -> r2 == r4 -> ratSubtract r1 r2 == ratSubtract r3 r4.
proof: Proof. intuition. unfold ratSubtract. rattac. inversion e0; clear e0; subst. inversion e; clear e; subst. arithNormalize. apply minus_eq_compat. arithSimplify. rewrite <- (Nat.mul_assoc n1). rewrite (Nat.mul_comm x2). rewrite Nat.mul_assoc. arithSimplify. trivial. rewrite <- (Nat.mul_assoc (n2 * x1)). rewrite (Nat.mul_comm x). rewrite Nat.mul_assoc. arithSimplify. rewrite <- (Nat.mul_assoc n2). rewrite (Nat.mul_comm x1 x0). rewrite Nat.mul_assoc. arithSimplify. rewrite Nat.mul_comm. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms