proposition: Lemma nth_elt_dbl_prop2 E n (f:= (Lf (nth_elt_dbl E n) n n)): natp n -> sub E n -> inc f (permutations n) /\ E = Vfs f (cardinal E).
proof: Proof. move => nN seN. set k := cardinal E. have SKN: sub E Nat by move => t /seN /(NS_inc_nat nN). move: (sub_smaller seN); rewrite -/k (card_card (CS_nat nN)) => lekn. move: (NS_le_nat lekn nN) => kN. move/setP_P: seN => seN. move: (nth_elt_dbl_prop nN seN) => [qa qb]; split => //. have si := (proj33 lekn); have scE: sub k (source f) by rewrite /f; aw. have ff: function f by apply: lf_function. set_extens t. move => tE. apply/(Vf_image_P ff scE). move: (nth_elt_surj SKN kN tE) => [i lik ->]; move/(NltP kN): (lik) => ik. by exists i => //; rewrite /f /nth_elt_dbl LfV//; [Ytac0 | apply: si ]. move/(Vf_image_P ff scE) => [i ik ->] . move: (si _ ik)=> iin; move/(NltP kN): ik=> lik. rewrite /f /nth_elt_dbl LfV//; Ytac0. apply:(nth_elt_inK (NS_lt_nat lik kN) SKN lik). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)