proposition: Lemma BQ_of_pair_prop1 a b (a' := a %/z (BZgcd a b)) (b' := b %/z (BZgcd a b)): intp a -> inc b BZps -> [/\ intp a', inc b' BZps, BZcoprime a' b' & BZBezout a' b'].
proof: Proof. move => az bzps. have bz:=(BZps_sBZ bzps). have bzp:=(BZps_sBZp bzps). have bnz:= (BZps_nz bzps). have hz: (a <> \0z \/ b <> \0z) by right. move:(BZ_positive_quo_gcd bzp az) (BZ_nz_quo_gcd bz az bnz). rewrite BZgcd_C => qp qnz. have b'zps: inc b' BZps by apply/BZps_iP. have a'zp:=(ZS_quo az (ZS_gcd az bz)). have bez:=(BZ_Bezout_cofactors az bz hz). by split => //; apply: BZ_coprime_if_Bezout => //; apply: BZps_sBZ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)