proposition: Lemma cnf_sort_correct E (x := cnf_sort E): cnf_rangep E -> cnfp x /\ range x = E.
proof: Proof. move => ha. suff: exists2 y, cnfp y & range y = E. move => [y yp1 yp2]. apply: (select_pr1 (p := fun t => cnfp t /\ range t = E)). exists y => //; apply/setP_P => t ty. move: yp1 => [hu hv _ _]; move: (domain_i1 ty) => pd. move: (in_graph_V hu ty) ->; apply: setXp_i. apply: (NS_inc_nat hv pd). by rewrite - yp2; apply: (inc_V_range hu pd). move => a b /= _ [ua ub] _ [uc ud]; rewrite - ud in ub. exact: (cnf_same_range ua uc ub). clear x. move /card_finite_setP: (proj31 ha). move: {2 3} (cardinal E) (erefl (cardinal E)) => n hb nN. move: n nN E ha hb; apply: Nat_induction. move => E _ ec ; exists \0f; first exact cnfp0. by rewrite (card_nonempty ec) range_set0. move => n nN Hrec E HE cardE. case: (emptyset_dichot E) => neE. by case:(@succ_nz n); rewrite - cardE neE cardinal_set0. move: HE => [fsE fgE mnE]. pose F := domain E. have fsF: finite_set F by apply: finite_fun_image. have neF: nonempty F by apply:funI_setne. have osF: ordinal_set F by move => i /funI_P [z /mnE/proj32 oi -> ]. move: (finite_subset_ord fsF neF osF) =>[e0 /funI_P [a aE av] e0p]. have amax: forall z, inc z E -> P z <=o P a. move => z zE; rewrite - av; apply: e0p; apply/funI_P; ex_tac. move: (esym(cpred_pr5 aE)); rewrite cardE (cpred_pr1 (CS_nat nN)). clear F fsF neF osF e0p. set F := E -s1 a; move => cardF. have sFE: sub F E by move => t/setC1_P []. have HF: cnf_rangep F. split. - exact: (sub_finite_set sFE fsE). - exact: (sub_fgraph fgE). - by move => x /sFE /mnE. move:(Hrec F HF cardF) => [x ox rx]. move/cnfpP: (ox) =>[fgx dxN qc qd]. move:(cnf_card_range ox); rewrite rx cardF => dxn. have ndx: ~ inc n (domain x) by rewrite dxn; apply:Nat_decent. set y := x +s1 (J n a). have dy: domain y = csucc n. by rewrite domain_setU1 (cnf_card_range ox) rx cardF (succ_of_nat nN). have fgy: fgraph y by apply: (fgraph_setU1 _ fgx ndx). have dyN: natp (domain y) by rewrite dy; apply:NS_succ. have y_out: Vg y n = a by apply:(setU1_V_out _ fgx ndx). have y_in i: i <c n -> Vg y i = Vg x i. by move => lin; apply:(setU1_V_in _ fgx ndx); rewrite dxn; apply/(NltP nN). exists y; last by rewrite range_setU1 rx; apply:setC1_K. have rb: forall i, inc i (domain y) -> omonomp (Vg y i). move => i;rewrite dy => /(NleP nN) /cle_eqVlt; case. by move ->; rewrite y_out; case: (mnE a aE). by move => id;rewrite (y_in i id); apply: qc;rewrite dxn; apply/(NltP nN). apply/cnfpP. split => // i iN; rewrite /oexp dy => /(cltSleP nN) /cle_eqVlt; case => lt1. have lin: i <c n by rewrite - lt1; exact:(cltS iN). have gxE: inc (Vg x i) F. rewrite - rx; apply: (inc_V_range fgx). by rewrite dxn; apply/(NltP nN). rewrite /oexp lt1 y_out (y_in _ lin); split. by apply:(amax _ (sFE _ gxE)). move/ (proj2 fgE _ _ (sFE _ gxE) aE) => ea. by move /setC1_P:gxE => /proj2. rewrite (y_in _ lt1) (y_in _ (clt_ltT (cltS iN) lt1)); apply: (qd i iN). by rewrite dxn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)