proposition: Lemma CNFq_p7 e c n : CNFq_ax e c n -> \1c <c n -> CNFbv e c \2c = cantor_mon e c \1c +o cantor_mon e c \0c.
proof: Proof. move=> ax n1; move:(cle_ltT cle_01 n1) => ha. by rewrite - succ_one (CNFq_p1 _ _ NS1) (CNFq_p3 (n:=n) ax). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)