proposition: Fact Op_lcmn_subproof n m : Z.of_nat (lcmn n m) = Z.lcm (Z.of_nat n) (Z.of_nat m).
proof: Proof. case: n m => [|n][|m]; rewrite ?lcmn0 // /lcmn /Z.lcm -Op_gcdn_subproof. case/dvdnP: (dvdn_gcdr n.+1 m.+1) => k {1 3}->. rewrite mulnA mulnK ?gcdn_gt0 // !Nat2Z.inj_mul Z_div_mult_full //; first nia. by case: (gcdn _ _) (gcdn_gt0 n.+1 m.+1). Qed.
imports: Coq(ZArith ZifyClasses ZifyInst ZifyBool) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(order binomial)