proposition: Lemma rat_remove_common_factor : forall (n num : nat)(nzn : nz n) den, RatIntro (n * num) (posnatMult (natToPosnat nzn) den) == RatIntro num den.
proof: Proof. rattac. inversion H; clear H; subst. arithNormalize. do 2 arithSimplify. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms