proposition: Lemma height_rcons v l : height (rcons v l) = height v + (if l == {{ then 1 else -1).
proof: Proof. rewrite /height /= !count_rcons. case: l; rewrite /= addn0 PoszD ?opprD ? addrA //. by rewrite -addrA [1 - _]addrC addrA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree