proposition: Lemma BQpsS_fromN_large e: inc e BQps -> exists2 n, natp n & BQinv (BQ_of_nat (csucc n)) <q e.
proof: Proof. move => ep. move:(QpsS_inv ep) => ies. move: (BQ_floorp4 (BQps_sBQ ies)) => [n na nb]. have nc:(BQ_of_nat n <q BQ_of_nat (csucc n)). by move/(qlt_cN na (NS_succ na)): (cltS na). move:(qlt_ltT nb nc) => h. move/(BQinv_mon2 (BQpsS_fromN na) ies):h; rewrite (BQinv_K (BQps_sBQ ep)) => h. by exists n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)