proposition: Lemma Typ_with_id_prop2 n S f x A: slistpl x n -> slistpl f n -> slistp A -> echelon S -> slength S <> \0c -> esize S <=c n +c slength A -> n = \0c -> echelon_can_extension S (Typ_with_id f A) = identity (echelon_of_base S (slist_append x A)).
proof: Proof. move => [xl sx] [lf sf] lA eS snt sS nz. have slAc:= (CS_nat (proj2 lA)). move: sS; rewrite nz (csum0l slAc) => eq1. move: (CS_nat (proj2 (proj1 (proj1 eS)))) => cb. have sp:=(card_ne0_pos cb snt). apply: (Eextension_prop_idL eS _ sp) => k kl. have kp:k <c domain A by apply: (clt_leT kl eq1). have hw:= (csum0l (proj31_1 kl)). have kda: inc k (domain A) by apply/(NltP (proj2 lA)). move: (slist_append_val2 xl lA kp); rewrite sx nz hw => ->. rewrite /Typ_with_id; set ff := Lg _ _. have lff: slistp ff by rewrite /ff;split; fprops; aw; exact (proj2 lA). have sff: slength ff = domain A by rewrite /ff/slength; aw. rewrite - sff in kp. by move: (slist_append_val2 lf lff kp); rewrite sf nz hw /ff LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)