proposition: Lemma BZgcd_A_alt 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. pose id3 u v w := Zo BZ (fun t=> exists x y z, [/\ intp x, intp y, intp z & t = u *z x +z (v *z y +z w *z z)]). have id3a: id3 a b c = id3 c a b. set_extens t => /Zo_P [tz [x [y [z [xz yz zz etc]]]]]; apply: Zo_i => //. exists z; exists x; exists y;split => //; rewrite etc (BZsumC (c *z z)). by apply:BZsumA; apply:ZSp. exists y; exists z; exists x; split => //;rewrite etc BZsumC. by symmetry;apply:BZsumA; apply: ZSp. have aux: forall u v w, inc u BZ -> inc v BZ -> inc w BZ -> BZ_ideal1 (BZgcd u (BZgcd v w)) = id3 u v w. move => u v w uz vz wz. move:(BZgcd_prop2 vz wz)=> [uu [vv [uuz vvz etc]]]. rewrite (proj2 (BZgcd_prop1 uz (ZS_gcd vz wz))). set_extens t; move => /Zo_P [tz h]; apply: (Zo_i tz). move: h => [c1 [c2 [c1z c2z ->]]]; rewrite etc. exists c1; exists (uu *z c2); exists (vv *z c2). rewrite (BZprodDl c2z (ZSp vz uuz) (ZSp wz vvz)). rewrite - (BZprodA vz uuz c2z) - (BZprodA wz vvz c2z). move: (ZSp uuz c2z)(ZSp vvz c2z) => sa sb; split => //. move: h=> [x [y [z [xz yz zz]]]]. move: (BZgcd_div vz wz). move: (ZS_gcd vz wz) => gz; move: (ZS_quo vz gz)(ZS_quo wz gz). set q1 := (v %/z BZgcd v w); set q2:=(w %/z BZgcd v w); set g := BZgcd v w. move => sa sb [-> ->]. move: (ZSp sa yz) (ZSp sb zz) => sc sd; move:(ZSs sc sd) => se. rewrite - (BZprodA gz sa yz) - (BZprodA gz sb zz). rewrite - (BZprodDr gz sc sd). move => ->; exists x; exists ((q1 *z y +z q2 *z z)); split => //. rewrite (BZgcd_C (BZgcd a b)). have pa:=(ZpS_gcd az (ZS_gcd bz cz)). have pb:= (ZpS_gcd cz (ZS_gcd az bz)). move: (aux _ _ _ az bz cz); rewrite id3a - (aux _ _ _ cz az bz). move => h; exact: (BZ_ideal_unique_gen1 pa pb h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)