proposition: Lemma esize_prop1 c (n:= esize c) (m:=slength c): echelon c -> \0c <c m -> [/\ natp n, \0c <c n, exists2 j, j <c m & Vg c j = J \0c n & forall j, j <c m -> P (Vg c j) = \0c -> Q (Vg c j) <=c n].
proof: Proof. move => ha hb. move: (echelon_p1 ha hb) => [b0 [b0N b0p cb0]]. have b4: Vg c \0c = J \0c b0 by rewrite - cb0 /Vl cpred1. rewrite /n/esize {n}; set r := range _ . move:ha =>[[pa pb] pc]. have mN := (proj2 pa). have rN: sub r Nat. move => v /Lg_range_P [i idc ->]; Ytac pz; last by apply: NS0. by move:(pb _ (inc_V_range (proj1 pa) idc)) => /setX_P []. have fsr: finite_set r. apply: (finite_range); aww. by rewrite - (NintE mN); apply: finite_Nint. have zd: inc \0c (domain c) by apply /(NltP mN). have b0r: inc b0 r by apply/Lg_range_P;exists \0c => //; rewrite b4; aw; Ytac0. have nr: nonempty r by exists b0. move: (finite_subset_Nat rN fsr nr) => [n nir nmax]. have nN:= (rN _ nir). have ->: union r = n. have csr: cardinal_set r by move => i /rN /CS_nat. apply: (cleA (card_ub_sup (CS_nat nN) nmax) (card_sup_ub csr nir)). have np:=(clt_leT b0p (nmax _ b0r)). split => //. move/Lg_range_P: (nir) => [b1 b1d]. move:(pb _ (inc_V_range (proj1 pa) b1d)) => /setX_P [qa qb qc]. Ytac fs => nn; last by move:(proj2 np); rewrite nn. by exists b1;[ apply /(slist_domainP pa) | rewrite - qa fs - nn ]. move => j ljm pz; apply:nmax; apply/Lg_range_P; exists j. by apply /(slist_domainP pa). by rewrite pz; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)