proposition: Lemma nth_elt_exten k f: natp k -> (forall i, i <c k -> natp (f i)) -> (forall i j, i <c j -> j <c k -> f i <c f j) -> (forall i, i<c k -> (nth_elt (fun_image k f) i = f i)).
proof: Proof. move => kN ha hb. set K := (fun_image k f). have Ka: sub K Nat by move => z /funI_P [i /(NltP kN) lik ->]; apply: ha. move:(Nintco_wor k) => [wor1 sr1]; move: (proj1 wor1) => or1. have csK: cardinal_set K by move => t /Ka /CS_nat. move:(wordering_cle_pr csK) => [[]]. set r2 := graph_on cardinal_le K => or2 _ sr2. have hc:lf_axiom f k K by move => t tk; apply/funI_P; ex_tac. have hd:function_prop (Lf f k K) k K. by saw; apply:lf_function. have he x y: inc y k -> (gle (Nint_co k) x y <-> x <=c y). move => /(NltP kN) yk; apply: (iff_trans(Nintco_gleP kN x y)). by split; first case. have hf x y: inc x K -> inc y K -> (x <=c y <-> gle r2 x y). move => xK yK; split => h; first by apply/graph_on_P1. by move/graph_on_P1: h => []. have finj:{inc k &, injective f}. move => i j /(NltP kN) lik /(NltP kN) ljk sf. case:(cleT_ell (proj31_1 lik) (proj31_1 ljk)) => // lij. - by case: (proj2 (hb _ _ lij ljk)); rewrite sf. - by case: (proj2 (hb _ _ lij lik)); rewrite sf. have hg: bijection_prop (Lf f k K) k K. by saw;apply:lf_bijective => // y /funI_P. have sf1: order_isomorphism (Lf f k K) (Nint_co k) r2. split => //; first by rewrite sr1 sr2 (NintE kN). hnf; aw => x y xK yK; rewrite !LfV//;apply:(iff_trans (he x y yK)). move: (hc _ xK) (hc _ yK) => fxk fyk. move/(NltP kN):(yK) => lyk;move/(NltP kN):(xK) => lxk. apply: (iff_trans _ (hf _ _ fxk fyk)). case:(cleT_ell (proj31_1 lxk) (proj31_1 lyk)) => lxy. - rewrite lxy; split => _; apply:cleR; first exact: (CS_nat (Ka _ fyk)). exact (proj31_1 lyk). - split => h; [ exact (proj1 (hb _ _ lxy lyk)) | exact:(proj1 lxy) ]. - by split => h; [ move:(cltNge lxy h) | case:(cltNge (hb _ _ lxy lxk) h)]. have Kb: cardinal K = k. by rewrite - (card_nat kN); apply:cardinal_fun_image. have aux: natp (cardinal K) by rewrite Kb. move:(nth_elt_ax Ka aux); rewrite Kb => hc'. have hd':function_prop (Lf (nth_elt K) k K) k K. by saw; apply:lf_function. have hg' : bijection_prop (Lf (nth_elt K) k K) k K. by saw; move:(proj1 (nth_elt_bf Ka aux)); rewrite Kb. have sf2: order_isomorphism (Lf (nth_elt K) k K) (Nint_co k) r2. split => //; first by rewrite sr1 sr2 (NintE kN). hnf; aw => x y xK yK; rewrite !LfV//;apply:(iff_trans (he x y yK)). move: (hc' _ xK) (hc' _ yK) => fxk fyk. move/(NltP kN):(yK) => lyk;move/(NltP kN):(xK) => lxk. apply: (iff_trans _ (hf _ _ fxk fyk)). case:(cleT_ell (proj31_1 lxk) (proj31_1 lyk)) => lxy. - rewrite lxy; split => _; apply:cleR; first exact: (CS_nat (Ka _ fyk)). exact (proj31_1 lyk). - split => h; last by exact:(proj1 lxy). have yb: y <c cardinal K by ue. exact: (proj1(nth_elt_monotone (NS_lt_nat lyk kN) Ka yb lxy)). - split => h; first by move:(cltNge lxy h). have xb: x <c cardinal K by ue. case:(cltNge (nth_elt_monotone (NS_lt_nat lxk kN) Ka xb lxy) h). move => i /(NltP kN) ik. move: (f_equal (Vf^~i) (iso_unique wor1 sf2 sf1)); rewrite !LfV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)