proposition: Lemma ratMult_inverse_nat : forall r1 r2 n d (nzn : nz n), r1 == r2 * (RatIntro n d) -> r1 * (RatIntro d (natToPosnat nzn)) == r2.
proof: Proof. intuition. eapply ratMult_inverse. rewrite H. eapply ratMult_eqRat_compat. intuition. eapply eqRat_terms; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms