proposition: Lemma BZdvd_latticeD: distributive_lattice1 BZdvdorder.
proof: Proof. suff: forall a b g z, inc a BZps -> inc b BZps -> inc g BZps -> inc z BZps -> BZBezout a b -> BZgcd z ((a *z b) *z g) %|z BZlcm (g *z a) (BZgcd (g *z b) z). move => h. apply:(proj32 (distributive_lattice_prop2 BZdvd_lattice)). apply /(distributive_lattice_prop3 BZdvd_lattice). move => x y z; rewrite BZdvdorder_sr => xs ys zs. rewrite (BZdvd_inf ys zs) (BZdvd_sup xs ys). move: (BZpsS_gcd ys zs) (BZpsS_lcm xs ys) (BZpsS_gcd xs ys)=> gs ls g1s. rewrite (BZdvd_inf zs ls) (BZdvd_sup xs gs). apply /BZdvdorder_gle; split; first by apply: (BZpsS_gcd zs ls). by apply: (BZpsS_lcm xs gs). move /BZps_iP: (xs)=> [xp xnz]; move: (BZp_sBZ xp) => xz. move /BZps_iP: (ys)=> [yp ynz]; move: (BZp_sBZ yp) => yz. move /BZps_iP: (g1s)=> [g1p g1nz]; move: (BZp_sBZ g1p) => g1z. move: (BZ_Bezout_cofactors xz yz (or_introl (y <> \0z) xnz)). move: (ZpS_quo xp g1p) (ZpS_quo yp g1p). rewrite (proj33 (BZlcm_prop1 xz yz)). move: (BZgcd_div xz yz) => []. set a := (x %/z BZgcd x y); set b := (y %/z BZgcd x y); set g := BZgcd x y. move => e1 e2 az bz; rewrite e1 e2. have ap: inc a BZps. by apply/BZps_iP; split => // aez; case: xnz; rewrite e1 aez BZprod_0r. have bp: inc b BZps. by apply/BZps_iP; split => // aez; case: ynz; rewrite e2 aez BZprod_0r. by apply: h. move => a b g z azp bzp gzp zzp bzt. set t := BZgcd g z. move: (BZpsS_gcd gzp zzp); rewrite -/t => /BZps_iP [tp tnz]. move: (BZps_sBZ gzp) (BZp_sBZ tp) => gz tz. move: (BZps_sBZ azp)(BZps_sBZ bzp)(BZps_sBZ zzp) => az bz zz. move /BZps_iP: gzp => [gp gnz]; move /BZps_iP: azp => [ap anz]. move /BZps_iP: bzp => [_ bnz]; move: (ZSp az bz) => abz. move: (ZSp gz az) (ZS_gcd (ZSp gz bz) zz) => pa pb. move: (BZgcd_div gz zz). move: (BZ_Bezout_cofactors gz zz (or_introl (z <> \0z) gnz)). set g' := (g %/z t); set z' := (z %/z t); move => bz1 [eq1 eq2]. move: (ZS_quo gz tz) (ZS_quo zz tz); rewrite -/g' -/z'; move => g'z z'z. move: (ZSp abz g'z) => abgz. move: (ZS_gcd z'z bz) => gs1. have ->: BZgcd z ((a *z b) *z g) = t *z BZgcd z' ((a *z b) *z g'). rewrite eq1 {1} eq2 -/t (BZprodC _ g'). rewrite (BZprodA abz g'z tz) (BZprodC _ t). rewrite (BZgcd_prodD z'z abgz tp); reflexivity. have cp1:BZcoprime z' g' by rewrite /BZcoprime BZgcd_C;apply: (BZ_coprime_if_Bezout g'z z'z bz1). have ->: BZgcd z' ((a *z b) *z g') = BZgcd z' ((a *z b)). rewrite BZprodC; apply: (BZgcd_simp z'z g'z abz cp1). move: (BZlcm_prop1 pa pb) => [_ _ ->]. have ->: BZgcd (g *z a) (BZgcd (g *z b) z) = t. rewrite /t (BZgcd_A (ZSp gz az)(ZSp gz bz) zz). rewrite (BZgcd_prodD az bz gp). move: (BZ_coprime_if_Bezout az bz bzt); rewrite /BZcoprime => ->. by rewrite (BZprod_1r gz). have ->: ((g *z a) %/z t) = g' *z a. rewrite eq1 -/t. rewrite - (BZprodA tz (ZS_quo gz tz) az). by rewrite (BZdvds_pr5 tz (ZSp g'z az) tnz). have ->: (BZgcd (g *z b) z %/z t) = BZgcd z' b. move: (ZSp g'z bz) => h. rewrite eq2 {1} eq1 -/t - (BZprodA tz g'z bz) (BZgcd_prodD h z'z tp) BZgcd_C. by rewrite (BZgcd_simp z'z g'z bz cp1) (BZdvds_pr5 tz gs1 tnz). suff: BZgcd z' (a *z b) %|z ((g' *z a) *z BZgcd z' b). rewrite (BZprodC t). move: (ZS_gcd z'z abz) (ZSp (ZSp g'z az) (ZS_gcd z'z bz)) => r1 r2. by move/ (BZdvds_prod r1 r2 tz tnz). rewrite - (BZprodA g'z az gs1). apply: (@BZdvds_trans (a *z BZgcd z' b)). apply: (BZdvds_pr1 g'z (ZSp az gs1)); apply:BZprod_nz => //. rewrite - (BZgcd_prodD z'z bz ap). move: (BZgcd_prop3 z'z abz)=> [[p1 p2 _ ] _]. move: (BZgcd_prop3 (ZSp az z'z) abz)=> [[_ _ p3] _ ]. apply: p3; last by apply: p2. apply: (@BZdvds_trans z'); [apply: (BZdvds_pr1 az z'z) | exact ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)