proposition: Lemma Bezout_pos_unique a b u v u' v': intp a -> intp b -> Bezout_pos a b u v -> Bezout_pos a b u' v' -> (u = u' /\ v = v').
proof: Proof. move => az bz [uz vzp ha hb] [u'z v'zp hc hd]. move:(Bezout_non_unique2 az bz uz (BZp_sBZ vzp) u'z (BZp_sBZ v'zp) hb hd). move => [q [qz sa]]. move: (ZS_sign a) (ZSa az) (BZp_sBZ v'zp) => saz aaz v'z. have qa:= (ZSp qz saz); have wz := (ZSo qa). rewrite (BZabs_sign az) (BZprodA qz saz aaz) /BZdiff. rewrite (BZopp_prod_l qa aaz) BZsumC; set w := (BZopp _) => eq1. case/BZ_i2P: (wz) => wp. move: (BZsum_Mp (ZSp wz aaz) vzp); rewrite - eq1 => qc. move: (BZprod_Mpp (BZabs_iN az) wp); rewrite BZprodC => qd. case: (zleNgt (zleT qd qc) hc). move: (BZopp_negative2 wp); rewrite (BZopp_K qa) => xp. move:(BZsum_diff_ea (ZSp wz aaz) (BZp_sBZ vzp) eq1). rewrite - (BZopp_prod_l qa aaz) /BZdiff (BZopp_K (ZSp qa aaz)) => eq2. move: (BZsum_Mp (ZSp qa aaz) v'zp); rewrite BZsumC - eq2 => qd. case: (equal_or_not (q *z BZsign a) \0z) => wnz; last first. move/BZps_iP: (conj xp wnz) => wp'. move: (BZprod_Mpp (BZabs_iN az) wp');rewrite BZprodC => qd'. case:(zleNgt (zleT qd' qd) ha). rewrite sa eq2 wnz BZprod_0l (BZsum_0r v'z); case: (equal_or_not q \0z) => eqz. by rewrite eqz BZprod_0l (BZsum_0r uz). move: wnz;case /(BZ_i1P): az. + move => az; move: ha; rewrite az BZabs_0 => /zgt0xP vn. case:(BZ_di_neg_pos vn vzp). + by move/BZsign_pos => ->; rewrite (BZprod_1r qz). + move/BZsign_neg => ->; rewrite (BZprod_m1r qz) => h. by case/(BZnon_zero_opp qz):eqz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)