proposition: Lemma echelon_of_base_of_tree t E: treep t -> echelon_of_base (tree_to_echelon t) E = tree_value E t.
proof: Proof. move:(tree_value_prop E) => [ha hb hc]. move: tree_to_echelon_E => [qa qb qc]. move: t;apply: tree_ind. - move => n nN. move:(NS_succ nN) (succ_positive n) => hu hv. rewrite (ha _ nN) (qa _ nN) echelon_of_baseE erecdef_base // /Vl. by rewrite (cpred_pr1 (CS_nat nN)). - move => x tx Hr. move:(tree_to_echelon_ok tx) => [sa sb sc]. by rewrite (qb _ tx) (hb _ tx) echelon_of_baseE erecdef_powerset // - Hr //. - move => x x' tx tx' Hx Hx'. move:(tree_to_echelon_ok tx) => [sa sb sc]. move:(tree_to_echelon_ok tx') => [sa' sb' sc']. rewrite (qc _ _ tx tx') (hc _ _ tx tx'). by rewrite echelon_of_baseE erecdef_product // -Hx// - Hx' //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)