proposition: Lemma echelon_recdef_extent2 c c' i: echelon c -> echelon c' -> i <=c slength c -> i <=c slength c' -> i <> \0c -> (forall k, k<c i -> Vg c k = Vg c' k) -> Vl (echelon_recdef c) i = Vl (echelon_recdef c') i.
proof: Proof. move => ec1 ec2 k1 k2 ip sv. have iN:=(NS_le_nat k1 (proj2 (proj1 (proj1 ec1)))). have lii: inc (cpred i) i by apply/(NltP iN); exact:(cpred_lt iN ip). have: echelon_recdef (restr c i) = echelon_recdef (restr c' i). congr echelon_recdef; apply: fgraph_exten; aww. by move => j ji /=; rewrite ! LgV//; apply: sv; apply/(NltP iN). rewrite (erecdef_restr ec1 k1) (erecdef_restr ec2 k2). by move/(f_equal (fun z => Vl z i)); rewrite /Vl LgV // => ->; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)