proposition: Theorem ratMult_eqRat_compat : forall (r1 r2 r3 r4 : Rat), eqRat r1 r2 -> eqRat r3 r4 -> eqRat (ratMult r1 r3) (ratMult r2 r4).
proof: Proof. rattac. repeat rewrite Nat.mul_assoc. rewrite <- (Nat.mul_assoc n1). rewrite (Nat.mul_comm n). rewrite Nat.mul_assoc. rewrite <- Nat.mul_assoc. rewrite e. rewrite e0. rewrite Nat.mul_assoc. do 3 arithSimplify. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms