proposition: Lemma OS_CNFp1 p n: CNFp_ax1 p n -> natp n -> ordinalp (CNFpv1 p n).
proof: Proof. move => ax nN; apply: (OS_oprodf nN) => // i lin. apply:(OS_CNFp0 ax lin). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)