proposition: Lemma ratMult_eq_rat1 : forall n1 n2 (nz1 : nz n1)(nz2 : nz n2), (n1 / n2) * (n2 / n1) == 1.
proof: Proof. intuition. rewrite <- ratMult_num_den. eapply num_dem_same_rat1. unfold posnatMult, natToPosnat, posnatToNat. eapply Nat.mul_comm. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms