proposition: Theorem num_dem_same_rat1 : forall n d, n = posnatToNat d -> RatIntro n d == rat1.
proof: Proof. rattac. inversion H0; clear H0; subst. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms