proposition: Lemma Bezout_non_unique1 a b u v: intp a -> intp b -> intp u -> intp v -> BZcoprime a b -> (a *z u) +z (b *z v) = \0z -> exists q, [/\ intp q, u = q *z b & v = BZopp(q *z a) ].
proof: Proof. move => az bz uz vz cab eq1. move:(BZ_Bezout_if_coprime az bz cab)=> [u' [v'[u'z v'z ha]]]. move:(ZSp az uz)(ZSp bz vz) (ZSp az u'z)(ZSp bz v'z)=> auz bvz au'z bv'z. case: (equal_or_not a \0z) => anz. move: ha eq1. rewrite /Bezout_rel anz ! BZprod_0l (BZsum_0l bvz) (BZsum_0l bv'z) => h. move: (BZprod_1_inversion_l bz v'z h) => [_ sb] pz. have sa: b *z b = \1z. case: sb => ->; first exact (BZprod_1r ZS1). by rewrite (BZprod_m1r ZSm1) BZopp_m1. move:(f_equal (fun z => b *z z) pz); rewrite (BZprodA bz bz vz) sa => sc. exists (u *z b); split. + by apply:ZSp. + by rewrite - (BZprodA uz bz bz) sa (BZprod_1r uz). + by move: sc;rewrite !BZprod_0r BZopp_0 (BZprod_1l vz). move:(BZdvd_correct vz az anz) => [qz rp [sc sd /BZp_sBZ rz]]. have hc:= ZSp qz bz; have wz := ZSs uz hc; have aqz := ZSp az qz. move: eq1. rewrite sc (BZprodDr bz aqz rz) (BZprodC b) - (BZprodA az qz bz). rewrite (BZsumA (ZSp az uz) (ZSp az hc) (ZSp bz rz)) - (BZprodDr az uz hc). move:(BZ_positive_quo_gcd rp az) (proj2 (BZgcd_div az rz)); rewrite BZgcd_C. move: (ZSo qz) => nqz qa qb qc. move: (BZgcd_rem az (ZSp bz rz) wz); rewrite BZsumC qc. rewrite (BZgcd_simp az bz rz cab) (BZgcd_zero az) => qd. have ww: inc (a *z (u +z (v %/z a) *z b)) BZ by apply:ZSp. case: (equal_or_not (v %%z a) \0z) => erz. exists (BZopp (v %/z a)); move:qc. rewrite erz BZprod_0r (BZsum_0r ww) (BZsum_0r aqz) => qc. rewrite (BZopp_prod_l nqz az) (BZopp_K qz) (BZprodC a); split => //. apply:(BZdiff_diag_rw uz (ZSp nqz bz)). rewrite /BZdiff - (BZopp_prod_l qz bz) (BZopp_K hc); ex_middle wnz. by case: (BZprod_nz az wz anz wnz). move: qa qb; rewrite - qd => qa qb. have qe: inc ((v %%z a) %/z BZabs a) BZps. by apply/BZps_iP; split => // ez; case: erz; rewrite qb ez BZprod_0r. move: (BZprod_Mpp (BZabs_iN az) qe);rewrite - qb => hh; BZo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)