proposition: Lemma dvdn_lcm d1 d2 m : lcmn d1 d2 %| m = (d1 %| m) && (d2 %| m).
proof: Proof. case: d1 d2 => [|d1] [|d2]; try by case: m => [|m]; rewrite ?lcmn0 ?andbF. rewrite -(@dvdn_pmul2r (gcdn d1.+1 d2.+1)) ?gcdn_gt0 // muln_lcm_gcd. by rewrite muln_gcdr dvdn_gcd {1}mulnC andbC !dvdn_pmul2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)