proposition: Lemma ratAdd_eqRat_compat_l : forall r1 r2 r3, eqRat r1 r2 -> r1 + r3 == r2 + r3.
proof: Proof. rattac. arithNormalize. f_equal. f_equal. rewrite Nat.mul_comm. rewrite (Nat.mul_comm _ x1). repeat rewrite Nat.mul_assoc. f_equal. rewrite Nat.mul_comm. rewrite e. apply Nat.mul_comm. do 3 arithSimplify. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms