proposition: Lemma ET_val3 c i (f := echelon_to_trees c) (a := (P (Vg c i))) (b := Q (Vg c i)): echelon c -> i <c (slength c) -> a <> \0c -> b <> \0c -> exists E F, [ /\ Tree_to_tree E = Vl f a, Tree_to_tree F = Vl f b& Tree_to_tree (Tproduct E F) = Vg f i ].
proof: Proof. move => ha hb az bz. move: (echelon_to_trees_prop ha) => [_ _ hd hc]. move: (hc _ hb) => [_ _ he3] {hc}; move: (he3 az bz) => []{he3}. rewrite -/a -/b => ha1 ha2 hb1 hb2 hf. have mN:= (proj2 (proj1 (proj1 ha))). have iN:= (NS_lt_nat hb mN). move: (cpred_pr6' iN ha1 ha2) => [sa sb sc]. move: (cpred_pr6' iN hb1 hb2) => [sa' sb' sc']. move: (Tree_to_tree_surjective (hd _(clt_ltT sc hb))) => [e ev]. move: (Tree_to_tree_surjective (hd _(clt_ltT sc' hb))) => [e' ev']. by exists e,e'; rewrite /f hf /Vl ev ev'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)