proposition: Lemma Eextension_prop_bijsetL c E E' f: echelon c -> \0c <c slength c -> (forall i, i <c esize c -> inc (Vg f i) (bijections (Vg E i) (Vg E' i))) -> inc (echelon_can_extension c f) (bijections (echelon_of_base c E) (echelon_of_base c E')).
proof: Proof. move => sa sb sc. rewrite /echelon_can_extension/echelon_of_base. have mN:= (slength_nat (proj1 (proj1 sa))). have hd:= (cpred_lt mN (nesym (proj2 sb))). exact: (Eextension_prop_bijset sa sc hd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)