proposition: Lemma is_yam_decr s : is_yam s -> is_yam (decr_yam s).
proof: Proof. elim: s => //= s0 s IHs /andP[Hpart]. move=> {}/IHs Hyam; case: s0 Hpart=> [// | s0'] /=. rewrite Hyam andbT evalseq_decr_yam. case H : (evalseq s) => [| sh0 sh] /= /andP[_] //=. by case s0'. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition