proposition: Lemma BZgcd_A a b c: intp a -> intp b -> intp c -> (BZgcd a (BZgcd b c)) = (BZgcd (BZgcd a b) c).
proof: Proof. move => az bz cz. move: (lattice_props (BZdvd_lattice)); rewrite BZdvdorder_sr. move =>[_ [_ [_ [_ [ _ [h _]]]]]]. have Ha t: intp t -> BZgcd \0z t = BZabs t. by move => rp; rewrite BZgcd_C BZgcd_zero. have Hb x y: intp x -> intp y -> BZabs (BZgcd x y) = BZgcd x y. move => xz yz; exact: (BZabs_pos (ZpS_gcd xz yz)). rewrite - (BZ_gcd_abs az (ZS_gcd bz cz)) (Hb _ _ bz cz). rewrite - (BZ_gcd_abs (ZS_gcd az bz) cz) (Hb _ _ az bz). rewrite - (BZ_gcd_abs az bz) - (BZ_gcd_abs bz cz). move: (BZabs_iN az) (BZabs_iN bz)(BZabs_iN cz). set x := BZabs a; set y := BZabs b; set z := BZabs c. move=> xp yp zp. move: (BZp_sBZ xp) (BZp_sBZ yp) (BZp_sBZ zp) => xz yz zz. case: (equal_or_not x \0z) => xnz. rewrite xnz (Ha y yz) (Ha _ (ZS_gcd yz zz)) (Hb _ _ yz zz). by rewrite (BZ_gcd_abs1 yz zz). case: (equal_or_not y \0z) => ynz. by rewrite ynz (Ha z zz) (BZgcd_zero xz) (BZabs_pos zp) (BZabs_pos xp). case: (equal_or_not z \0z) => znz. rewrite znz (BZgcd_zero yz) (BZgcd_zero (ZS_gcd xz yz)) (Hb _ _ xz yz). by rewrite (BZ_gcd_abs2 xz yz). have xx:inc x BZps by apply/BZps_iP. have yy:inc y BZps by apply/BZps_iP. have zza:inc z BZps by apply/BZps_iP. move: (h _ _ _ xx yy zza). rewrite (BZdvd_inf yy zza) (BZdvd_inf xx yy). rewrite (BZdvd_inf xx (BZpsS_gcd yy zza)). by rewrite (BZdvd_inf (BZpsS_gcd xx yy) zza). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)