proposition: Lemma position_in_cnf_prop x d (k := position_in_cnf x d): cnfp x -> ordinalp d -> [/\ k <=c domain x, forall i, i <c k -> oexp x i <o d & k = domain x \/ d <=o oexp x k].
proof: Proof. move => ox od; rewrite /k/ position_in_cnf; clear k. set n := domain x; set E := Zo _ _. have nN:= proj42 ox. have Eb: forall t, inc t (E +s1 n) -> t <=c n. move => t /setU1_P; case;first by move/Zo_S /(NltP nN) /proj1. move => ->; apply: (cleR (CS_nat nN)). have ha: sub (E +s1 n) Nat by move => y /Eb lyn; apply: (NS_le_nat lyn nN). have hb: nonempty (E +s1 n) by exists n; fprops. move: (inf_Nat ha hb); set k := intersection _;move => [ kE hd]. move:(Eb _ kE)(ha _ kE) => lekn kN. split => //; last by case/setU1_P: kE => h; [ right; move/Zo_hi: h | left]. move => t ltk; have td: inc t (domain x) by apply/(NltP nN); apply: (clt_leT ltk lekn). have oe: ordinalp (oexp x t). by move/cnfpP: ox => /proj43 h; case: (h _ td). case: (oleT_el od oe) => h //. have /hd/cleNgt []//: inc t (E +s1 n) by apply:setU1_r; apply:Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)