proposition: Theorem complete_leaves_height t : complete t -> leaves t = 2 ^ height t.
proof: Proof. elim: t => //= t1 IH1 t2 IH2. move/andP => [H_c H_h]. move/andP: H_c => [H_c1 H_c2]. move/eqP: H_h => H_h. rewrite IH1 // IH2 // H_h /maxn. case: ifP; last by rewrite expnS mulSn mul1n. by rewrite ltnNge; move/negP. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq)