proposition: Lemma Typ_with_id_prop n S f x y A : slistpl x n -> slistpl y n -> slistpl f n -> slistp A -> echelon S -> slength S <> \0c -> esize S <=c n +c slength A -> (forall i, i <c n -> inc (Vg f i) (bijections (Vg x i) (Vg y i))) -> inc (echelon_can_extension S (Typ_with_id f A)) (bijections (echelon_of_base S (slist_append x A)) (echelon_of_base S (slist_append y A)) ).
proof: Proof. move => [lx sx][ly sy] [lf sf] lA eS snt sS hd. rewrite /echelon_can_extension /echelon_of_base. have he:=(cpred_lt (proj2 (proj1 (proj1 eS))) snt). apply:(Eextension_prop_bijset eS _ he) => j jle. rewrite /Typ_with_id; set ff := Lg _ _. have nN: natp n by rewrite - sf; exact (proj2 lf). have lAN: natp (domain A) by exact: (proj2 lA). have lff: slistp ff by rewrite /ff; split; aw; fprops. move:(clt_leT jle sS); rewrite csumC => jsa. have jN: natp j by exact: (NS_lt_nat jsa (NS_sum lAN nN)). case:(NleT_el nN jN) => js. move: (cdiff_pr js) => js1; rewrite - js1. have js3:=(cdiff_Mlt lAN jN js jsa). have js2: j -c n <c slength ff by rewrite /ff; aw. have js4: inc (j -c n) (domain A) by apply/(NltP lAN). rewrite -{1} sf (slist_append_val2 lf lff js2). rewrite -{2} sx (slist_append_val2 lx lA js3). rewrite -{3} sy (slist_append_val2 ly lA js3). rewrite /ff LgV//; apply/bijectionsP; rewrite/bijection_prop; aw; split => //. exact: identity_fb. have sl': j <c slength f by rewrite sf. have sx': j <c slength x by rewrite sx. have sy': j <c slength y by rewrite sy. rewrite (slist_append_val1 lf lff sl'). rewrite (slist_append_val1 lx lA sx'). by rewrite (slist_append_val1 ly lA sy'); apply: hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)