proposition: Lemma egcdzP m n : egcdz_spec m n (egcdz m n).
proof: Proof. rewrite /egcdz; have [-> | m_nz] := eqVneq. by split; [rewrite -abszEsign gcd0z | rewrite coprimezE absz_sign]. have m_gt0 : (`|m| > 0)%N by rewrite absz_gt0. case: egcdnP (coprime_egcdn `|n| m_gt0) => //= u v Duv _ co_uv; split. rewrite !mulNr -!mulrA mulrCA -abszEsg mulrCA -abszEsign. by rewrite -!PoszM Duv addnC PoszD addrK. by rewrite coprimezE abszM absz_sg m_nz mul1n mulNr abszN abszMsign. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly ssrnum ssrint archimedean rat matrix) mathcomp(polydiv perm zmodp mxalgebra vector)