proposition: Lemma CNFp_1 p n: CNFp_ax1 p n -> \0c <c n -> CNFpv1 p \1c = cantor_pmon p \0c.
proof: Proof. move => ax1 n1; rewrite /CNFpv1 oprod_f1 //. apply: (OS_CNFp0 ax1 n1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)