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