proposition: Lemma ratInverse_prod_1 : forall r, ~ r == 0 -> (ratInverse r) * r == 1.
proof: Proof. intuition. unfold ratInverse. destruct r. destruct n. exfalso. eapply H. eapply rat_num_0. rewrite <- ratMult_num_den. eapply num_dem_same_rat1. unfold posnatMult, natToPosnat, posnatToNat. destruct p. apply Nat.mul_comm. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms