proposition: Lemma tree_value_commutes E c (f := echelon_value c E) (t :=echelon_to_trees c) (g := Lg (domain c) (fun i => (tree_value E (Vg t i)))): echelon c -> f = g.
proof: Proof. move => ec; symmetry. have mN:= (proj2(proj1(proj1 ec))). move:(echelon_to_trees_prop ec); rewrite -/t; move => [ta tb tc td]. have ha: domain g = slength c by rewrite /g; aw. have ndg: natp (domain g) by rewrite ha. have hb: slistpl g (slength c) by split => //; split => //; rewrite /g; fprops. apply: (erecdef_unique1 ec hb). move => i il; move:(td _ il) => /= [ua ub uc]. have idc: inc i (domain c) by apply/(NltP mN). have iN:= (NS_lt_nat il mN). split. - move => w; move:(ua w) =>[sa sb sc]; rewrite /g LgV// sc. rewrite (proj31 (tree_value_prop E)) //. exact: (proj31(cpred_pr6' (NS_esize ec) sa sb)). - move => w; move: (ub w) => [sa sb sc]. move:(cpred_pr6' iN sa sb)=> [pa pb pc]. have lt2:= (clt_ltT pc il). have cpd: inc (cpred (P (Vg c i))) (domain c) by apply/(NltP mN). rewrite /g /Vl LgV// LgV// sc// (proj32 (tree_value_prop E)) //. by apply: tc. - move => w1 w2;move: (uc w1 w2) => [sa sb sa' sb' sc]. move:(cpred_pr6' iN sa sb)=> [pa pb pc]. move:(cpred_pr6' iN sa' sb')=> [pa' pb' pc']. have lt2:= (clt_ltT pc il). have cpd: inc (cpred (P (Vg c i))) (domain c) by apply/(NltP mN). have lt2':= (clt_ltT pc' il). have cpd': inc (cpred (Q (Vg c i))) (domain c) by apply/(NltP mN). rewrite /g /Vl LgV// LgV// LgV//. by rewrite sc// (proj33 (tree_value_prop E) _ _ (tc _ lt2) (tc _ lt2')). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)