proposition: Lemma echelon_p1' c: echelon c -> \0c <c slength c -> exists b, [/\ natp b, \0c <c b & Vg c \0c = J \0c b].
proof: Proof. move => h1 h2; move: (echelon_p1 h1 h2) => [n [bN bp v]]; exists n; split=> //. by rewrite -v /Vl cpred1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)