proposition: Lemma rat_mult_den : forall n d1 d2, (RatIntro n (posnatMult d1 d2)) == (RatIntro 1 d1) * (RatIntro n d2).
proof: Proof. intuition. assert (n = 1 * n)%nat. lia. rewrite H at 1. apply ratMult_num_den; lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms