proposition: Lemma nds_sc_Kval n c K: natp n -> inc K (\Po n) -> nds_sc_K c K = csumb K c.
proof: Proof. move => nN /setP_P Kb. rewrite /nds_sc_K. have KN: sub K Nat by move => t tK; move:(NS_inc_nat nN (Kb _ tK)). set q := cardinal K; set f := nth_elt K. have qN: natp q by apply:(sub_nat_finite nN Kb). have ha: forall i, i <c q -> inc (f i) K. move => i iq; apply:(nth_elt_inK (NS_lt_nat iq qN) KN iq). have: forall j, inc j K -> exists2 i, i <c q & j = f i. move => j jK; apply: (nth_elt_surj KN qN jK). have : forall i j, i <c q -> j <c q -> f i = f j -> i = j. move => i j /(NltP qN) iq /(NltP qN) jq. move:(proj2 (proj1 (proj1(nth_elt_bf KN qN)))). have ax: lf_axiom (nth_elt K) (cardinal K) K. by move => t /(NltP qN) /ha. aw => h; move: (h i j iq jq); rewrite !LfV//. have: finite_set K by apply/NatP. move: q qN (f) (K) ha; clear. apply: Nat_induction. move => k K _ _ _ sf. have h: domain (Lg K c) = emptyset. by aw; apply /set0_P => t /sf [i /clt0]. by rewrite csumb0 /csumb (csum_trivial h). move => n nN Hrec f K fK fsK fi fs. rewrite (csum_fs _ nN). have nn:= (cltS nN). move:(fK _ nn) => fnK. move: (setC1_K fnK); set K1:= K -s1 (f n) => Kv. have h1: forall i, i <c n -> inc (f i) K1. move => i lin; move:(clt_ltT lin nn) => h; move: (fK _ h). rewrite - Kv =>/setU1_P; case => // eq; move:(fi _ _ h nn eq) => ein. by case: (proj2 lin). have h2:=(sub_finite_set (@sub_setC K (singleton (f n))) fsK). have h4: forall i j, i <c n -> j <c n -> f i = f j -> i = j. move => i j lin ljn;apply (fi _ _ (clt_ltT lin nn) (clt_ltT ljn nn)). have h5:forall j, inc j K1 -> exists2 i : Set, i <c n & j = f i. move => j /setC1_P [/fs [i /(cltSleP nN) lin ->] h]. case: (equal_or_not i n) => ein; first by case: h; rewrite ein. by exists i. have fnk1:~ inc (f n) K1 by move/setC1_P=> [ _ ]. by rewrite (Hrec f K1 h1 h2 h4 h5) - Kv (csumA_setU1 _ fnk1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)