proposition: Lemma nth_elt_dbl_prop1 n K (k := cardinal K) (s:= (Lf (nth_elt_dbl (K +s1 n) (csucc n)) (csucc n) (csucc n))): natp n -> inc K (\Po n) -> [/\ inc s (permutations (csucc n)), k <=c n, K = fun_image k (Vf s), Vf s k = n & (forall i j, i<c j -> j <c k -> (Vf s i) <c (Vf s j))].
proof: Proof. move => nN KP. move: (NS_succ nN) => sN. move/setP_P:KP => sKn. have KF1: sub (K +s1 n) (csucc n). move:(cleS nN) => /ocle /proj33 snn t /setU1_P []; first by move /sKn /snn. by move => ->; apply/Nsucc_i. move/setP_P: (KF1) => KF. have SKN: sub (K +s1 n) Nat by move => t /KF1 / (NS_inc_nat sN). move: (nth_elt_dbl_prop sN KF); rewrite -/s; move => [ax sp]. have nK: ~inc n K by move/sKn; apply:Nat_decent. move: (csucc_pr nK); rewrite -/k => cK'. move:(sub_smaller sKn); rewrite (card_nat nN) -/k => lekn. have kN:= (NS_le_nat lekn nN). have k1N: natp (cardinal (K +s1 n)) by rewrite cK'; apply: (NS_succ kN). have kl1 := cltS kN. have ha i: i <c (csucc k) -> Vf s i = nth_elt (K +s1 n) i. move => lik; rewrite /s LfV//; first by rewrite /nth_elt_dbl cK'; Ytac0. by apply/(NltP sN); apply/(clt_leT lik); apply: cleSS. have hb: forall x, inc x (K+s1 n) -> exists2 i, i <c (csucc k) & x = Vf s i. move => x xK; move: (nth_elt_surj SKN k1N xK); rewrite cK'. by move => [i lik ->]; rewrite -(ha _ lik); exists i. have hc: forall i j, i <c j -> j <c (csucc k) -> Vf s i <c Vf s j. move => i j lij ljk; rewrite (ha _ ljk) (ha _ (clt_ltT lij ljk)). apply:(nth_elt_monotone (NS_lt_nat ljk (NS_succ kN)) SKN _ lij); ue. have hd: forall i, i <c (csucc k) -> inc (Vf s i) (K +s1 n). move => i lik; rewrite (ha _ lik). apply:(nth_elt_inK (NS_lt_nat lik (NS_succ kN)) SKN); ue. have sk: Vf s k = n. move:(hb _ (setU1_1 K n)) =>[ i lin nv]. move: lin=> /(cltSleP kN) / cle_eqVlt; case; [ by move <- | move => lik]. move: (hc _ _ lik kl1); rewrite - nv; move => [np1 np2]. move: (hd _ kl1) => /setU1_P; case => //. by move/sKn/(NltP nN) /cltNge; case. have hu i j: i <c j -> j <c k -> Vf s i <c Vf s j. move => lij ljk; apply: hc => //; exact:(clt_ltT ljk kl1). split => //. set_extens t. move => tK; move: (hb _ (setU1_r n tK)) => [i ilk e1]. move: ilk=> /(cltSleP kN) / cle_eqVlt; case => ee. by case: nK; rewrite - sk - ee - e1. by rewrite e1; apply: funI_i; apply/NltP. move/funI_P => [i /(NltP kN) lik ->]. case /setU1_P: (hd _ (clt_ltT lik (cltS kN))) => // eq1. by move: (hc _ _ lik kl1); rewrite eq1 sk; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)