proposition: Lemma erecdef_restr c n: echelon c -> n <=c slength c -> echelon_recdef (restr c n) = restr (echelon_recdef c) n.
proof: Proof. move => ha hb; symmetry. move: (ha) => [[[pa pb] pc] pd]. have dr: domain (restr c n) = n by aw. have sid: sub n (domain c) by exact:(proj33 hb). have nN := NS_le_nat hb pb. have hc: slist_E (restr c n) (Nat \times Nat). split; first by split; fprops; rewrite dr. exact: (sub_trans (restr_range1 pa sid) pc). have hd: echelon (restr c n). split => // i; rewrite /slength dr => lin. have in': inc i n by apply/(NltP nN). by rewrite LgV//; apply: pd; apply: (clt_leT lin hb). have he:slistpl (restr (echelon_recdef c) n) (slength (restr c n)). by rewrite /slistpl /slength !Lgd; split => //; split=> //;fprops; aw. apply: (erecdef_unique hd he); aw => i lin. have in': inc i n by apply/(NltP nN). have iN:= (NS_lt_nat lin nN). have lin': i <c slength c by exact: (clt_leT lin hb). move: (erecdef_prop ha) => [ra rb rc]. rewrite LgV // (rc _ lin'); rewrite LgV //. apply:erecdef_prop1 => // j ji. by move/(NltP nN):(clt_ltT ji lin) => ljn; rewrite [in RHS] LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)