proposition: Lemma regular_cnext x: infinite_c x -> regular_cardinal (cnext x).
proof: Proof. move/ord_index_pr1 => [sa <-]. rewrite (cnextE sa); exact:regular_initial_successor. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)