proposition: Lemma CR_prop3 n: natp n -> inc (CR_next_term f n) BQp.
proof: Proof. move => nN; case: (CR_prop2 nN) => ->; first by apply: QpS0. apply:(BQps_sBQp (CR_prop0 nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)