proposition: Lemma Eextension_prop_inj c f (g := echelon_extension c f): echelon c -> (forall i, i <c (esize c) -> injection (Vg f i)) -> (forall i, i <c (slength c) -> injection (Vg g i)).
proof: Proof. move => ha hc i im. move: (slength_nat (proj1 (proj1 ha))) => mN. have iN:= (NS_lt_nat im mN); move: i iN im. apply: Nat_induction1 => k kN Hr lkn. move: (Eextension_prop f ha lkn); simpl;set a := P _; set b := Q _. move => [pa pb pc]. case (p_or_not_p (a = \0c)) => az. move: (pa az) => [/cge1P ra rb ->]. apply: (hc _(cpred_pr0 ra rb (NS_esize ha))). case (p_or_not_p (b = \0c)) => bz. move: (pb bz) => [ra rb ->]. move:(cpred_pr6' kN ra rb) =>[qa qb qc]. apply: etp_fi; apply:Hr => //; apply: (clt_ltT qc lkn). move:(pc az bz) => [ra rb rc rd ->]. move:(cpred_pr6' kN ra rb) (cpred_pr6' kN rc rd)=>[qa qb qc][qa' qb' qc']. apply: ext_to_prod_fi; apply: Hr => //. apply: (clt_ltT qc lkn). apply: (clt_ltT qc' lkn). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)