proposition: Lemma Tree_to_tree_prop e (t := Tree_to_tree e): [/\ treep t, tdepth t = nat_to_B (Tdepth e), tree_size t = nat_to_B (Tsize e)& tree_is_pos t <-> Tpositive e].
proof: Proof. rewrite /t {t};elim:e. - move => n /=; move: (nat_to_B_Nat n) => sa;move:(proj31 tdepth_prop_inv _ sa). move => [sc sd];rewrite(proj31 tree_size_p _ sa). move:(proj31 tree_to_pos_p2 _ sa) => h. split => //; apply: (iff_trans h); case: (n); first by split. move => m; split => //= _; exact: succ_nz. - move => e [ha hb hc hd] /=. rewrite (proj32 tree_size_p _ ha). have he:=(iff_trans (proj32 tree_to_pos_p2 _ ha) hd). move:(proj32 tdepth_prop_inv _ ha) => [hf ->]; rewrite hb; split => //. - move => e [ha hb hc hd] e' [ha' hb' hc' hd'] /=. rewrite (proj33 tree_size_p _ _ ha ha'). move:(proj33 tdepth_prop_inv _ _ ha ha') => [he ->]. have hf:= (proj33 tree_to_pos_p2 _ _ ha ha'). rewrite hb hb' hc hc' !(nat_to_B_max); split => //. split; first by move/hf => [/hd -> /hd' ->]. by move/andP => [/hd hd1 /hd' hd2]; apply/hf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)