proposition: Lemma echelon_trivial_value n (S:= slist1 (J \0c n)) E: natp n -> n <> \0c -> echelon_of_base S E = (Vl E n).
proof: Proof. move => nN np. move: (slist1_prop (J \0c n)) => [[ha hb] hc]. move:(echelon_trivial nN np) => [pa pb]. rewrite /echelon_of_base hb /Vl cpred1. have w1: \0c <c slength S by rewrite hb; exact: clt_01. move: (proj31 (echelon_value_prop E pa w1)); rewrite hc; aw => h1. by case: (h1 (erefl \0c)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)