proposition: Fact iter_lcmn_div (n m : nat) : (0 < n)%N -> (n <= m)%N -> n %| l m.
proof: Proof. move=> lt0n lenm; apply: dvdn_trans (iter_lcmn_leq_div lenm); rewrite /iter_lcmn. rewrite (@big_cat_nat _ _ _ n) //= big_nat1; exact: dvdn_lcmr. Qed.
imports: mathcomp(all_ssreflect all_algebra)