proposition: Lemma size_hyper_yam ev : size (hyper_yam ev) = sumn ev.
proof: Proof. elim/last_ind: ev => //= sh sn. rewrite /hyper_yam -(sumn_rev (rcons _ _)) rev_rcons /= size_cat => ->. by rewrite size_nseq sumn_rev. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition