proposition: Lemma is_add_corner_yam l0 s : is_yam (l0 :: s) -> is_add_corner (evalseq s) l0.
proof: Proof. rewrite /is_add_corner /=; case: l0 => [// | l0] /=. case: (evalseq s) => [| sh0 sh] /andP[]. move=> /andP[H1 H2] _; exfalso. by case: l0 H1 H2 => //= l0 _; elim: l0. move=> /is_partP[_ /( _ l0)] /=. rewrite -/(incr_nth (sh0 :: sh) l0.+1) !nth_incr_nth eq_refl add1n. by rewrite eq_sym ltn_eqF // add0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition