proposition: Lemma erecdef_powerset c (c' := Ech_powerset c): echelon c -> \0c <c slength c -> echelon_recdef_last c' = h2 ( echelon_recdef_last c).
proof: Proof. rewrite/echelon_recdef_last => ec cp. move:(Ech_powerset_prop ec cp) => [ha hb hc hd he]. rewrite /c' hb /Vl (cpred_pr1 (proj32_1 cp)). have p1: (slength c) <c slength (Ech_powerset c). rewrite hb; apply: cltS; exact: (proj2 (proj1 (proj1 ec))). move: (proj32 (erecdef_prop2 ha p1)); rewrite hd; aw => hh. move: (hh (erefl \0c)) => [ka kb ->]; congr h2. apply:(echelon_recdef_extent2 ha ec (proj1 p1) kb (nesym (proj2 cp)) he). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)