proposition: Theorem ratAdd_eqRat_compat : forall r1 r2 r3 r4, eqRat r1 r2 -> eqRat r3 r4 -> r1 + r3 == r2 + r4.
proof: Proof. intuition. eapply eqRat_trans. eapply ratAdd_eqRat_compat_l; eauto. repeat rewrite (ratAdd_comm r2). eapply ratAdd_eqRat_compat_l; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms