proposition: Lemma muln_lcmr : right_distributive muln lcmn.
proof: Proof. case=> // m n p; rewrite /lcmn -muln_gcdr -!mulnA divnMl // mulnCA. by rewrite muln_divA ?dvdn_mull ?dvdn_gcdr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)