proposition: Lemma BQpair_mon C n m: BQpair_aux C -> natp m -> n <c m -> P (Vg C n) <q P (Vg C m) /\ Q (Vg C m) <q Q (Vg C n).
proof: Proof. move => [pa pb pc pd pe] mN lt1. have nN:=(NS_lt_nat lt1 mN). move/(cleSltP nN): lt1 => mn. rewrite - (cdiff_pr mn). move:(NS_diff (csucc n) mN); move: (m -c (csucc n)); apply: Nat_induction. rewrite csum0r; fprops; split; fprops. move => k kN [Hr1 Hr2]. have h := (NS_sum (NS_succ nN ) kN). move: (pd _ h)(pe _ h) => ha hb. rewrite (csum_nS _ kN); split; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)