proposition: Lemma BZlcm_prop2 a b (l := BZlcm a b): intp a -> intp b -> [/\ a %|z l, b %|z l & forall u, a %|z u -> b %|z u -> l %|z u].
proof: Proof. move => az bz ; rewrite /l. move: (BZlcm_prop1 az bz) => [pa pb pc]. move: (ZS_gcd az bz) => gz. split; first by rewrite pb BZprodC; apply: (BZdvds_pr1 (ZS_quo bz gz) az). by rewrite pa; apply: (BZdvds_pr1 (ZS_quo az gz) bz). move => u ua ub. case: (equal_or_not a \0z) => anz. move: ua; rewrite anz; move /BZdvds_trivial_rec => ->. rewrite BZlcm_C (BZlcm_zero bz); exact (proj1(BZdvd_zero1 ZS0)). have h: a <> \0z \/ b <> \0z by left. move: (BZdvds_pr ua) (BZdvds_pr ub) => r1 r2. move: (BZ_Bezout_cofactors az bz h) => [x [y [xz yz eq1]]]. move: (f_equal (fun z => z *z u) eq1). move:(ua) => [uz _ _]. move: (ZS_quo az gz) (ZS_quo bz gz). set a' := (a %/z BZgcd a b); set b' := (b %/z BZgcd a b). move => a'z b'z. move:(ZS_quo uz bz)(ZS_quo uz az) (ZS_lcm az bz) => ubz uaz lz. move: (ZSp xz ubz)(ZSp yz uaz) => aaz bbz. rewrite (BZprod_1l uz) (BZprodDl uz (ZSp a'z xz) (ZSp b'z yz)) => <-. set a1 := (a' *z x) *z u ; set a2 := (b' *z y) *z u. have ->: a2 = y *z ((u %/z a) *z BZlcm a b). rewrite /a2 (BZprodC _ u) (BZprodA uz b'z yz). by rewrite {1} r1 (BZprodC a) -(BZprodA uaz az b'z) - pb BZprodC. have ->: a1 = x *z ((u %/z b) *z BZlcm a b). rewrite /a1 (BZprodC _ u) (BZprodA uz a'z xz). by rewrite {1} r2 (BZprodC b) -(BZprodA ubz bz a'z) (BZprodC b) pa BZprodC. rewrite (BZprodA yz uaz lz) (BZprodA xz ubz lz) - (BZprodDl lz aaz bbz). apply: (BZdvds_pr1 (ZSs aaz bbz) lz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)