proposition: Lemma lcmn_swap a b c : a * c = b * (a + c) -> lcmn b c = lcmn a c.
proof: Proof. case: a => [|a]. by move/eqP; rewrite add0n eq_sym muln_eq0=> /orP[] /eqP->; rewrite !(lcm0n,lcmn0). case: b => [|b]. by move/eqP; rewrite muln_eq0=> /orP[] /eqP->; rewrite !(lcm0n,lcmn0). case: c => [|c H]. by move/eqP; rewrite addn0 eq_sym muln0 muln_eq0=> /orP[] /eqP->; rewrite !(lcm0n,lcmn0). apply/eqP. have /eqn_pmul2r<- : a.+1 * gcdn b.+1 c.+1 > 0 by rewrite muln_gt0 gcdn_gt0. rewrite {2}muln_gcdr H [b.+1 * _]mulnC mulnDl gcdnDl. rewrite mulnCA muln_lcm_gcd -muln_gcdl !mulnA. by rewrite muln_lcm_gcd [X in _ == X]mulnAC. Qed.
imports: mathcomp(all_ssreflect)