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