proposition: Lemma Z2int_lcm x y : Z.le 0 x -> Z.le 0 y -> Z2int (Z.lcm x y) = lcmn `|Z2int x| `|Z2int y|.
proof: Proof. case: x => [|x|//] _; [by rewrite /= lcm0n|]. case: y => [|y|//] _; [by rewrite /= lcmn0|]. rewrite /Z.lcm Z2int_abs Z2int_mul Z2int_div //. rewrite ZgcdE' abszM; apply: f_equal; apply/eqP. rewrite -(@eqn_pmul2r (gcdn `|Z2int (Z.pos x)| `|Z2int (Z.pos y)|)); last first. { rewrite gcdn_gt0; apply/orP; left; rewrite absz_gt0 /= eqz_nat. apply: lt0n_neq0; exact: nat_of_pos_gt0. } rewrite muln_lcm_gcd. rewrite -(absz_nat (gcdn _ _)) -mulnA -abszM. rewrite Z2int_Z_of_nat /=. by rewrite intdiv.divzK // /mem /in_mem /intdiv.dvdz /= dvdn_gcdr. Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)