proposition: Lemma BZgcd_rem a b q: intp a -> intp b -> intp q -> BZgcd a (b +z a *z q) = BZgcd a b.
proof: Proof. move => az bz qz. suff: BZ_ideal2 a b = BZ_ideal2 a (b +z a *z q) by rewrite /BZgcd => ->. move: (ZSp az qz) => aqz. set_extens t => /Zo_P [pa [u [v [uz vz etc]]]]; apply:Zo_i => //. move:(ZSp vz qz) => vqz; move: (ZS_diff uz vqz)=> ha. exists (u -z v *z q); exists v;split => //. move: (ZSp aqz vz)=> pa1. rewrite (BZprodBr az uz vqz) (BZprodDl vz bz aqz). rewrite (BZprodC v) (BZprodA az qz vz). rewrite (BZsum_ACA (ZSp az uz)(ZSo pa1) (ZSp bz vz) pa1) - etc. by rewrite (BZsumC _ ((a *z q) *z v)) - /(_ -z _) (BZdiff_diag pa1) BZsum_0r. move : etc; rewrite (BZprodDl vz bz aqz) (BZsumC (b *z v)). rewrite (BZsumA (ZSp az uz) (ZSp aqz vz) (ZSp bz vz)) - (BZprodA az qz vz). move: (ZSp qz vz) => qvz. rewrite -(BZprodDr az uz qvz) => ->. by exists (u +z q *z v); exists v; split => //; apply: ZSs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)