proposition: Lemma lem_mlcm m m1 m2 : (mlcm m1 m2 <= m)%MM = (m1 <= m)%MM && (m2 <= m)%MM.
proof: Proof. apply/forallP/andP => [H|[/forallP H1 /forallP H2] i]; first split. - by apply/forallP=> i; apply: leq_trans (H i); rewrite mnmE leq_maxl. - by apply/forallP=> i; apply: leq_trans (H i); rewrite mnmE leq_maxr. by rewrite mnmE geq_max H1 H2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg