proposition: Lemma nth_elt_dbl_prop K n: natp n -> inc K (\Po n) -> lf_axiom (nth_elt_dbl K n) n n /\ inc (Lf (nth_elt_dbl K n) n n) (permutations n).
proof: Proof. move => nN /setP_P sKn. have snn: sub n Nat by move => t /(NS_inc_nat nN). have sKN:= sub_trans sKn snn. move: (sub_nat_finite nN sKn) => kN. move: (@sub_setC n K)=> pa. move:(cardinal_setC2 sKn). rewrite (card_nat nN) - csum2cr - csum2cl => w. have ax: lf_axiom (nth_elt_dbl K n) n n. rewrite /nth_elt_dbl. move => i /(NltP nN) lin; move: (NS_lt_nat lin nN) => iN. case: (NleT_el kN iN) => ha; [ rewrite (Y_false (cleNgt ha)) | Ytac0]. move:(NS_diff (cardinal K) iN) => diN. apply: (pa). apply:(nth_elt_inK diN (sub_trans pa snn)). by apply:(csum_lt2l kN diN (sub_nat_finite nN pa));rewrite (cdiff_pr ha)-w. apply: sKn;apply:(nth_elt_inK iN sKN ha). split => //; apply/permutationsP; saw. apply:bijective_if_same_finite_c_surj; aw; trivial. by apply: finite_set_nat. apply: (lf_surjective ax) => y yn. case: (inc_or_not y K) => yK. move:(nth_elt_surj sKN kN yK) => [i lik ->]; exists i. move: (sub_smaller sKn); rewrite (card_nat nN) => le1. apply/(NltP nN); apply: (clt_leT lik le1). by rewrite /nth_elt_dbl; Ytac0. have yK': inc y (n -s K) by apply/setC_P. have sKN':= sub_trans pa snn. move:(nth_elt_surj sKN' (sub_nat_finite nN pa) yK')=> [i lik ->]. exists (i +c (cardinal K)). by apply/(NltP nN); rewrite w csumC; apply/csum_Meqlt. rewrite /nth_elt_dbl Y_false. by rewrite (cdiff_pr1' (proj31_1 lik) kN). by apply/cleNgt; apply:(Nsum_Mle0 _ kN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)