proposition: Lemma rat_num_nz : forall n d, n > 0 -> RatIntro n d == 0 -> False.
proof: Proof. rattac. unfold posnatToNat, natToPosnat in *. destruct d. simpl in *. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms