proposition: Lemma last_yam y : is_yam y -> last 0 y = 0.
proof: Proof. case/lastP: y => //= y yn. rewrite last_rcons. elim: y => [// | y0 y IHy] /=. case: yn => [// | y] /= /andP[H _]. by elim: y H => [// | yn IHy] /= /IHy. by move=> /andP[_]; exact IHy. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition