proposition: Lemma Eextension_prop_composable c f f' (g := echelon_extension c f) (g' := echelon_extension c f'): echelon c -> (forall i, i <c esize c -> (Vg f' i) \coP (Vg f i)) -> forall i,i <c (slength c) -> (Vg g' i) \coP (Vg g i).
proof: Proof. move => h ha. have nN:=(NS_esize h); set n := esize c. pose E := Lg n (fun i => source (Vg f i)). pose E' := Lg n (fun i => target (Vg f i)). pose E'' := Lg n (fun i => target (Vg f' i)). have hb: (forall i, i <c n -> inc (Vg f i) (functions (Vg E i) (Vg E' i))). move => i lin; move:(ha _ lin) => [_ fa _];apply/functionsP; split => //. by rewrite /E LgV//; apply /(NltP nN). by rewrite /E' LgV//; apply /(NltP nN). have hc: (forall i, i <c n -> inc (Vg f' i) (functions (Vg E' i) (Vg E'' i))). move => i lin; move:(ha _ lin) => [fa _ fb];apply/functionsP; split => //. by rewrite /E' LgV//; apply /(NltP nN). by rewrite /E'' LgV//; apply /(NltP nN). move => i lim. move: (Eextension_prop_fct h hc lim) => /functionsP [ra rb rc]. move: (Eextension_prop_fct h hb lim) => /functionsP [ra' rb' rc']. by split => //;rewrite rb rc'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)