proposition: Lemma lcmnA : associative lcmn.
proof: Proof. move=> m n p; rewrite [LHS]/lcmn [RHS]/lcmn mulnC. rewrite !divn_mulAC ?dvdn_mull ?dvdn_gcdr // -!divnMA ?dvdn_mulr ?dvdn_gcdl //. rewrite mulnC mulnA !muln_gcdr; congr (_ %/ _). by rewrite ![_ * lcmn _ _]mulnC !muln_lcm_gcd !muln_gcdl -!(mulnC m) gcdnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)