proposition: Lemma ratAdd_num : forall n1 n2 d, RatIntro (n1 + n2) d == (ratAdd (RatIntro n1 d) (RatIntro n2 d)).
proof: Proof. rattac. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms