proposition: Lemma OS_cnf_degree x: cnfp_nz x -> ordinalp (cnf_degree x).
proof: Proof. move => xnz; move: (cnf_size_nz_bis xnz) => si. by move /cnfpP: (proj1 xnz) => [_ _ qa _]; case:(qa _ si). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)