proposition: Lemma ratInverse_ratMult : forall r1 r2, ~ r1 == 0 -> ~ r2 == 0 -> ratInverse (r1 * r2) == ratInverse r1 * ratInverse r2.
proof: Proof. intuition. unfold ratInverse. destruct r1. destruct n. exfalso. eapply H. eapply rat_num_0. destruct r2. destruct n0. exfalso. eapply H0. eapply rat_num_0. case_eq (RatIntro (S n) p * RatIntro (S n0) p0); intuition. inversion H1; clear H1; subst. unfold ratMult. unfold natToPosnat, posnatToNat, posnatMult. simpl. eapply eqRat_terms. destruct p. destruct p0. trivial. simpl. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms