proposition: Lemma nth_elt_bf K (f := Lf (nth_elt K) (cardinal K) K): sub K Nat -> natp (cardinal K) -> (bijection f /\ forall i j, inc i (source f) -> inc j (source f) -> i <c j -> Vf f i <c Vf f j).
proof: Proof. move => KN kN. move: (nth_elt_ax KN kN) => ax. have sf: source f = (cardinal K) by rewrite /f;aw. have pa: forall i j, inc i (source f) -> inc j (source f) -> i <c j -> Vf f i <c Vf f j. rewrite /f;aw;move => i j isf jsf; rewrite !LfV //. move/(NltP kN): jsf => jk. by apply:nth_elt_monotone => //; apply:(NS_lt_nat jk kN). split; last by exact. rewrite sf in pa. move: (finite_set_nat kN) => fsk. rewrite /f;apply: bijective_if_same_finite_c_inj; aw; trivial. split; first by apply:lf_function. rewrite sf => i j iK jK sv. case: (NleT_ell (NS_inc_nat kN iK) (NS_inc_nat kN jK)) => cp //. by case: (proj2 (pa _ _ iK jK cp)). by case: (proj2 (pa _ _ jK iK cp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)