proposition: Lemma is_rem_corner_yam l0 s : is_yam (l0 :: s) -> is_rem_corner (evalseq (l0 :: s)) l0.
proof: Proof. move/is_yam_tl/is_part_eval_yam/is_partP => [_ Hpart]. rewrite /is_rem_corner !nth_incr_nth ltn_eqF // eq_refl add0n add1n ltnS. exact: Hpart. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition