proposition: Lemma OS_cnf_rem x : cnfp x -> ordinalp (cnf_rem x).
proof: Proof. move => [_ nN _ [[pa pb pc pd] pe]]. move : (NS_pred nN) => pN. move: (cpred_le (CS_nat nN)) => le1. apply: (OS_CNFb (NS_pred nN)); split. split. - exact: pa. - move => i lin;exact: (pb i (clt_leT lin le1)). - move => i lin;exact: (pc i (clt_leT lin le1)). - move => i iN lin; exact: (pd i iN (clt_leT lin le1)). move => i lin;exact: (pe i (clt_leT lin le1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)