proposition: Lemma BZ_Bezout_cofactors a b: intp a -> intp b -> (a<> \0z \/ b <> \0z) -> BZBezout (a %/z (BZgcd a b)) (b %/z (BZgcd a b)).
proof: Proof. move => az bz h. move:(BZgcd_prop2 az bz); set g := (BZgcd a b); move => [x [y [xz yz]]]. move: (BZgcd_div az bz) => []; rewrite -/g => p1 p2. rewrite {1} p1 {1} p2; set qa := (a %/z g); set qb:= (b %/z g). move: (BZp_sBZ (ZpS_gcd az bz)) => gz. move: (ZS_quo az gz) (ZS_quo bz gz) => pa pb. rewrite - (BZprodA gz pa xz) - (BZprodA gz pb yz). rewrite - (BZprodDr gz (ZSp pa xz) (ZSp pb yz)). rewrite/g - {1} (BZprod_1r gz) => h1. exists x; exists y;split => //; symmetry. by apply: (BZprod_eq2l ZS1 _ gz (BZgcd_nz1 az bz h) h1); apply:ZSs; apply:ZSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)