proposition: Lemma BQpair_aux2a_equiv C: BQpair_aux C -> ( BQpair_aux2a C <-> BQpair_aux2b C).
proof: Proof. move => cpa; split; last by move => H n nn; apply: H. move => H n m nN mN. have qa: n <c csucc (n +c m). apply /cltSleP; fprops; apply:csum_M0le; fprops. have qb: m <c csucc (n +c m). rewrite csumC;apply /cltSleP; fprops; apply:csum_M0le; fprops. have sN := (NS_succ (NS_sum nN mN)). have ha:=(proj1 (BQpair_mon cpa sN qa)). move:(proj2 (BQpair_mon cpa sN qb)) (H _ sN) => hb hc. exact: (qlt_ltT(qlt_ltT ha hc) hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)