proposition: Lemma BQ_of_pair_prop2 a b c d: intp a -> inc b BZps -> intp c -> inc d BZps -> BZBezout a b -> BZBezout c d -> a *z d = b *z c -> a = c /\ b = d.
proof: Proof. move => az bzp cz dzp b1 b2 eq1. have dz := (BZps_sBZ dzp). have bz:= (BZps_sBZ bzp). have bnz:= (BZps_nz bzp). have dnz:= (BZps_nz dzp). have lbd: gle BZdvdorder b d. apply/BZdvdorder_gle; split => //. have [u [v [uz vz eq2]]]:= b1. have auz:= ZSp az uz. have avz:= ZSp bz vz. have cuz:= ZSp cz uz. have dvz:= ZSp dz vz. move: (BZprod_1r dz); rewrite - eq2 BZprodDr // BZprodA // (BZprodC d) eq1. rewrite (BZprodC b v) BZprodA // - BZprodA // (BZprodC b) - BZprodDl // => <-. by apply:BZdvds_pr1 => //; apply: ZSs. have ldb: gle BZdvdorder d b. apply/BZdvdorder_gle; split => //. have [u [v [uz vz eq2]]] := b2. have auz:=ZSp az uz. have avz := ZSp az vz. have cuz:= ZSp cz uz. have dvz:= ZSp dz vz. have bvz:= ZSp bz vz. move: (BZprod_1r bz); rewrite -eq2 BZprodDr// BZprodA// -eq1 (BZprodC _ d). rewrite - BZprodA// (BZprodC d) (BZprodC d) BZprodA// - BZprodDl// => <-. by apply:BZdvds_pr1 => //; apply: ZSs. have ebd:= (order_antisymmetry (proj1 BZdvd_lattice) lbd ldb). by move: eq1; rewrite ebd BZprodC;move/ (BZprod_eq2l az cz dz dnz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)