proposition: Lemma BQ_of_pair_prop5 a b c d: intp a -> inc b BZps -> intp c -> inc d BZps -> (a *z d = b *z c <-> BQ_of_pair a b = BQ_of_pair c d).
proof: Proof. move => az bp cz dp. apply:(iff_trans (BQ_of_pair_prop3 az bp cz dp)); split. by move => [e1 e2]; rewrite /BQ_of_pair -lock /BQ_of_pair_internal e1 e2. rewrite /BQ_of_pair -lock /BQ_of_pair_internal => e1. split; first exact: (pr1_def e1). move: (BQ_of_pair_prop1 az bp) => [_ qb _ _]. move: (BQ_of_pair_prop1 cz dp) => [_ qa _ _]. by rewrite -(BZp_hi_pr (BZps_sBZp qb)) -(BZp_hi_pr (BZps_sBZp qa)) (pr2_def e1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)