proposition: Fact iter_lcmn_gt0 (n : nat) : (l n > 0)%N.
proof: Proof. elim: n => [|n ihn]; first by rewrite iter_lcmn0. by rewrite /iter_lcmn (@big_cat_nat _ _ _ n.+1) //= lcmn_gt0 ihn big_nat1. Qed.
imports: mathcomp(all_ssreflect all_algebra)