proposition: Lemma ratInverse_nz : forall (r : Rat), ratInverse r == 0 -> False.
proof: Proof. intuition. unfold ratInverse in *. rattac. destruct n0. unfold posnatToNat, natToPosnat in *. destruct p. destruct p0. inversion H0; clear H0; subst. rewrite Nat.mul_1_r in e. rewrite Nat.mul_1_r in e. lia. unfold posnatToNat, natToPosnat in *. destruct p. destruct p0. inversion H0; clear H0; subst. rewrite Nat.mul_1_r in e. rewrite Nat.mul_0_l in e. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms