proposition: Lemma nds_tn_C_exten Z Y n: natp n -> same_below Z Y n -> nds_tn_C Z n = nds_tn_C Y n.
proof: Proof. move => nN h. have aux: forall K s, inc K (\Po n) -> inc s (permutations (cardinal K)) -> nds_sc_Ktau Z K s = nds_sc_Ktau Y K s. move => K s /setP_P Kb /permutationsP [[[fs _] _ ] ss tf]. have fsK:=(sub_finite_set Kb (finite_set_nat nN)). have ckN: natp (cardinal K) by apply /NatP. have sKN:=(sub_trans Kb (NS_inc_nat nN)). apply:(osumf_exten ckN) => i lin; apply: h. have h1: Vf s i <c cardinal K. by apply /(NltP ckN); Wtac; rewrite ss;apply /(NltP ckN). apply/(NltP nN); apply: Kb; apply: (nth_elt_inK (NS_lt_nat h1 ckN) sKN h1). rewrite /nds_tn_C /nds_tn_S; apply: f_equal. set_extens t; move => /setUf_P [K KP /funI_P [s sp ->]]; apply /setUf_P; ex_tac; apply/funI_P;first ex_tac. exists s; [ done | symmetry;exact:(aux K s KP sp)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)