proposition: Lemma hyper_yamP ev : is_part ev -> is_yam (hyper_yam ev).
proof: Proof. elim/last_ind: ev => // s sn IHs. rewrite /hyper_yam rev_rcons /=; case: sn => [| sn]. by move/is_partP; rewrite last_rcons /= => [] []. elim: sn => [/= | sn /= IHsn]. move=> Hpart1; have Hpart := is_part_rconsK Hpart1. by rewrite (IHs Hpart) size_rev (evalseq_hyper_yam Hpart) incr_nth_size Hpart1. move=> Hpart2. move/(_ (part_rcons_ind Hpart2))/andP : IHsn => [-> ->]; rewrite !andbT. by have:= Hpart2; rewrite -{1}(evalseq_hyper_yam Hpart2) /hyper_yam rev_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition