proposition: Lemma erecdef_base n (c := Ech_base n): natp n -> \0c <c n -> echelon_recdef_last c = h1 n.
proof: Proof. move => sa sb. move: (Ech_base_prop sa sb) =>[ha hb hc hd]. have slc: slength c = \1c; rewrite /slength /c/Ech_base; aw; trivial. rewrite /echelon_recdef_last /Vl slc cpred1. have sz: \0c <c slength c by rewrite slc; exact : clt_01. move:(proj31 (erecdef_prop2 ha sz)); rewrite hb; aw => h. exact: (proj33 (h (erefl \0c))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)