proposition: Lemma Echelon_value_ex1 E (A := Vg E \0c): echelon_of_base Echelon_ex1 E = \Po (A \times A) /\ echelon_can_extension Echelon_ex1 E = \Pof (A \ftimes A).
proof: Proof. move:(proj1 Tree_ex1_prop ) => xx. move:(tree_value_prop E) => [ha hb hc]. move:(tree_extension_prop E) => [ha' hb' hc']. move: (tdepth_prop_inv) => [qa qb qc]. move: (proj1 (qa _ NS0)) => ta. move: (proj1 (qc _ _ ta ta)) => tb. rewrite /Echelon_ex1 (echelon_of_base_of_tree E xx) /Tree_ex1. rewrite (hb _ tb) (hc _ _ ta ta) (ha _ NS0). rewrite (can_extension_of_tree E xx). by rewrite (hb' _ tb) (hc' _ _ ta ta) (ha' _ NS0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)