proposition: Lemma height_cons l v : height (l :: v) = (if l == {{ then 1 else -1) + height v.
proof: Proof. rewrite /height /=; case: l; rewrite /= add0n !PoszD !addrA //. by rewrite opprD /= addrA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree