proposition: Theorem rat_num_S : forall n d, (RatIntro (S n) d == (RatIntro 1 d) + RatIntro n d)%rat.
proof: Proof. intuition. rattac. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms