proposition: Lemma height_nseq n b : height (nseq n b) = Posz n * (if b == {{ then 1 else -1).
proof: Proof. elim: n => [|n IHn] /=; rewrite !height_simpl ?mul0r // IHn. by rewrite -[X in X + _]mul1r -mulrDl -PoszD add1n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree