proposition: Lemma right_sizes_left_comb n : right_sizes (leftcomb n) = nseq n 0.
proof: Proof. elim: n => //= n ->. by rewrite -[RHS]cat1s -[[:: 0]]/(nseq 1 0) -!nseqD addnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype