proposition: Lemma Eextension_prop_idL c f E: echelon c -> (forall i, i <c esize c -> (Vg f i) = identity (Vg E i)) -> \0c <c slength c -> (echelon_can_extension c f) = identity (echelon_of_base c E).
proof: Proof. set n := esize c; move => ha hb hc. have hd:(forall i, i <c n-> Vg f i = identity (source (Vg f i))). by move => i lin; rewrite (hb _ lin); aw. have hd': (forall i, i <c n -> inc (Vg f i) (functions (Vg E i) (Vg E i))). by move => i lin; rewrite(hb _ lin);apply/functionsP; apply: identity_prop. have mN:= (slength_nat (proj1 (proj1 ha))). have he:= (cpred_lt mN (nesym (proj2 hc))). move: (Eextension_prop_id ha hd he). by move /functionsP: (Eextension_prop_fct ha hd' he)=> [_ -> _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)