proposition: Lemma BZlcm_prop1 a b (g := BZgcd a b) (l := BZlcm a b): intp a -> intp b -> [/\ l = (a %/z g) *z b, l = a *z (b %/z g) & l = ((a %/z g) *z (b %/z g)) *z g].
proof: Proof. move => az bz. move: (ZS_gcd az bz) => gz. case:(equal_or_not b \0z) => bnz. rewrite /l bnz (BZlcm_zero az) BZprod_0r. by rewrite (proj2 (BZ_quorem00 gz)) !BZprod_0r BZprod_0l. move: (BZgcd_div az bz); rewrite -/g. set q1:= (a %/z g); set q2 := (b %/z g); move => [pa pb]. move: (ZS_quo az gz) (ZS_quo bz gz) => q1z q2z. suff: l = q1 *z b. move => ->;split => //; rewrite pb ? pa. by rewrite (BZprodA q1z gz q2z) (BZprodC g _). by rewrite (BZprodC g _) (BZprodA q1z q2z gz). rewrite/l/BZlcm{1} pa -(BZprodA gz q1z bz); apply:(BZdvds_pr5 gz (ZSp q1z bz)). by apply: (BZgcd_nz1 az bz); right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)