proposition: Lemma iter_lcmn_mul_rat (r : rat) (n : nat) : `|denq r| <= n -> (iter_lcmn n)%:Q * r \is a Qint.
proof: Proof. move=> ledn; rewrite -[r]divq_num_den mulrA -rmorphM. by apply/Qint_dvdz/dvdz_mulr/iter_lcmn_div; rewrite // absz_gt0 denq_neq0. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics binomialz bigopz arithmetics seq_defs a_props