proposition: Lemma Eextension_prop_fct 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) (functions (Vg E i) (Vg E' i))) -> forall i, i <c (slength c) -> inc (Vg g i) (functions (Vg A i) (Vg A' i)).
proof: Proof. move => ha hb i im. move: (slength_nat (proj1 (proj1 ha))) => mN. have iN:= (NS_lt_nat im mN); move: i iN im. apply: Nat_induction1. move => i iN Hr lim. move: (Eextension_prop f ha lim) (echelon_value_prop E ha lim) (echelon_value_prop E' ha lim). simpl;set a := P _; set b := Q _; rewrite -/A -/A' -/g. move => [pa pb pc][pa' pb' pc'][pa'' pb'' pc'']. case (p_or_not_p (a = \0c)) => az. move: (pa az) (pa' az) (pa'' az) => [/cge1P ra rb ->][_ _ ->] [_ _ ->]. apply: (hb _(cpred_pr0 ra rb (NS_esize ha))). case (p_or_not_p (b = \0c)) => bz. move: (pb bz) (pb' bz) (pb'' bz) => [ra rb ->][_ _ ->] [_ _ ->]. move: (cpred_pr6' iN ra rb) =>[qa qb qc]. apply: etp_fun; apply:Hr => //; exact: (clt_ltT qc lim). move:(pc az bz) (pc' az bz)(pc'' az bz) => [ra rb rc rd ->][_ _ _ _ ->] [_ _ _ _ ->]. move: (cpred_pr6' iN ra rb) (cpred_pr6' iN rc rd) =>[qa qb qc][qa' qb' qc']. apply: ext_to_prod_fun; apply: Hr => //. apply: (clt_ltT qc lim). apply: (clt_ltT qc' lim). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)