proposition: Lemma esize_prop2 c n (m:=slength c): echelon c -> (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) -> esize c = n.
proof: Proof. move => ha [j ja jb] hc. have mp:= (cle_ltT (cle0x (proj31_1 ja)) ja). move:(esize_prop1 ha mp); set k := esize c. move => [kN kp [j2 j2a j2b] hd]. apply: cleA. have pa:P (Vg c j2) = \0c by rewrite j2b; aw. by move: (hc _ j2a pa); rewrite j2b; aw. have pa:P (Vg c j) = \0c by rewrite jb; aw. by move: (hd _ ja pa); rewrite jb; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)