proposition: Lemma BQ_of_pair_neg a b: inc a BZm -> inc b BZps -> inc (BQ_of_pair a b) BQm.
proof: Proof. move => azn bzps; move: (BZm_sBZ azn) => az. have ->: (BQ_of_pair a b) = BQopp (BQ_of_pair (BZopp a) b). by rewrite - (BQ_of_pair_opp (ZSo az) bzps) (BZopp_K az). apply:BQopp_positive2; apply:(BQ_of_pair_pos (BZopp_negative2 azn) bzps). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)