proposition: Lemma Tree_ex2_prop : treep Tree_ex2 /\ tree_size Tree_ex2 = \0c.
proof: Proof. move:tdepth_prop_inv => [ha hb hc]. move:tree_size_p => [qa qb qc]. move:(proj1 (ha _ NS0)) (qa _ NS0) => r1 r2. move:(proj1 (hc _ _ r1 r1)) (qc _ _ r1 r1); rewrite r2 cmax00 => r3 r4. move:(proj1 (hc _ _ r3 r1)) (qc _ _ r3 r1); rewrite r2 r4 cmax00 => r5 r6. split; [exact:(proj1 (hb _ r5)) | by move:(qb _ r5); rewrite r6 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)