proposition: Lemma Eextension_prop_comp c f f' E E' E'' (m := slength c) (n:= esize c) (f'' := Lg n (fun z => (Vg f' z) \co (Vg f z))) (g := echelon_extension c f) (g' := echelon_extension c f') (g'':= echelon_extension c f''): echelon c -> (forall i, i <c n -> inc (Vg f i) (functions (Vg E i) (Vg E' i))) -> (forall i, i <c n -> inc (Vg f' i) (functions (Vg E' i) (Vg E'' i))) -> forall i, i <c m -> Vg g'' i = (Vg g' i) \co (Vg g i).
proof: Proof. move => ha hb hc. set (A := echelon_value c E). set (A' := echelon_value c E'). set (A'':= echelon_value c E''). have hb': forall i, i <c m -> inc (Vg g i) (functions (Vg A i) (Vg A' i)). by move => i lim; apply: Eextension_prop_fct. have hc': forall i, i <c m -> inc (Vg g' i) (functions (Vg A' i) (Vg A'' i)). by move => i lim; by apply: Eextension_prop_fct. move: (slength_nat (proj1 (proj1 ha))) => mN i lim. have iN:= (NS_lt_nat lim mN); move: i iN lim. have nN:=(NS_esize ha). apply: Nat_induction1. move => k kN Hr lt. move: (Eextension_prop f ha lt) (Eextension_prop f' ha lt) (Eextension_prop f'' ha lt). simpl;set a := P _; set b := Q _. 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 ->] [_ _ ->] [_ _ ->]. move: (cpred_pr0 ra rb nN) => w. by rewrite /Vl /f'' LgV//; apply /(NltP nN). case (p_or_not_p (b = \0c)) => bz. move: (pb bz)(pb' bz)(pb'' bz) => [ra rb ->] [ _ _ ->][_ _ ->]. move:(cpred_pr6' kN ra rb) =>[qa qb qc]; have W:= (clt_ltT qc lt). move: (hb' _ W) (hc' _ W) => i1 i2. by rewrite /Vl -/g -/g' - (etp_comp i1 i2) - (Hr _ qc W). move:(pc az bz)(pc' az bz) (pc'' az bz) => [ra rb rc rd ->] [_ _ _ _ ->] [ _ _ _ _ ->]. move:(cpred_pr6' kN ra rb) (cpred_pr6' kN rc rd)=>[qa qb qc][qa' qb' qc']. have W := (clt_ltT qc lt); have W' := (clt_ltT qc' lt). move:(Hr _ qc W) (Hr _ qc' W') => i1 i2. move:(hc' _ W)(hb' _ W)(hc' _ W') (hb' _ W')=> ia ib ic id. by rewrite /Vl (ext_to_prod_comp ib id ia ic) /f'' i1 i2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)