proposition: Lemma cnf_exponents_of x (E := cnf_exponents x): cnfp x -> (finite_set E /\ ordinal_set E).
proof: Proof. move => ox. have aux: cardinal (cnf_exponents x) = domain x. rewrite (cnf_card_range ox). by apply: cardinal_fun_image; move: (proj2 (cnf_range_fgraph ox)). split. apply/NatP; rewrite aux; exact: (proj42 ox). move => t /funI_P [z /(range_gP (proj41 ox)) [i idy ->]->]. by apply: (proj42 (proj1 (proj44 ox))); apply/(NltP (proj42 ox)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)