proposition: Lemma Bezout_non_unique2 a b u v u' v': intp a -> intp b -> intp u -> intp v -> intp u' -> intp v' -> Bezout_rel a b u v -> Bezout_rel a b u' v' -> exists q, [/\ inc q BZ, u' = u +z q *z b & v' = v -z q *z a].
proof: Proof. move => az bz uz vz u'z v'z eq1 eq2. have cp: BZcoprime a b by apply: BZ_coprime_if_Bezout => //; exists u,v. move:(ZSp az uz)(ZSp az u'z)(ZSp bz vz)(ZSp bz v'z)=> auz au'z bvz bv'z. move: (BZdiff_diag ZS1); rewrite - {1} eq2 - eq1. rewrite (BZdiff_diff2 (ZSs au'z bv'z) auz bvz). rewrite /BZdiff (BZsum_AC au'z bv'z (ZSo auz)). rewrite - /(BZdiff (a *z u') _) - (BZprodBr az u'z uz). rewrite - (BZsumA (ZSp az (ZS_diff u'z uz)) bv'z (ZSo bvz)). rewrite - /(BZdiff _ _) - (BZprodBr bz v'z vz) => H. move:(Bezout_non_unique1 az bz (ZS_diff u'z uz) (ZS_diff v'z vz) cp H). by move => [q [qz ha hb]]; exists q; rewrite - ha -hb !BZsum_diff. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)