proposition: Lemma Eextension_prop_bijset c E E' f (A := echelon_value c E) (A' := echelon_value c E') (g := echelon_extension c f): echelon c -> (forall i, i <c (esize c) -> inc (Vg f i) (bijections (Vg E i) (Vg E' i))) -> forall i, i <c (slength c) -> inc (Vg g i) (bijections (Vg A i) (Vg A' i)).
proof: Proof. move => ha hb i hc. apply: Zo_i; first by apply: (Eextension_prop_fct ha) hc; move => j /hb /Zo_P[]. have ra:(forall i, i <c esize c -> bijection (Vg f i)). by move => j /hb /Zo_P[]. by case:(Eextension_prop_bij_inv ha ra hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)