proposition: Lemma Ech_base_prop n (c:= Ech_base n): natp n -> \0c <c n -> [/\ echelon c, Vg c \0c = J \0c n, \0c <c slength c & esize c = n].
proof: Proof. move => ha hb. have nz:=(nesym (proj2 hb)). have i01: inc \0c \1c by apply: set1_1. have lt01 := clt_01. have ns1 := NS1. have vz: Vg c \0c = J \0c n by rewrite /c/Ech_base;rewrite LgV. have r0: slength c = \1c by rewrite /c /Ech_base /slength Lgd. have hc: echelon c. split; last by rewrite r0 => i /clt1 ->; rewrite vz; aw; split. rewrite /c/Ech_base; split; first split; aww. move => i /Lg_range_P[_ _ ->]; apply: setXp_i => //; apply: NS0. have sp: \0c <c slength c by rewrite /slength/c /Ech_base Lgd. split => //. apply: (esize_prop2 hc). by exists \0c => //; rewrite r0. move => j; rewrite r0 /c/Ech_base => /(NltP NS1)jz; rewrite ! LgV//; aw. move => _; exact: (cleR (CS_nat ha)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)