proposition: Lemma part_rcons_ind s sn : is_part (rcons s sn.+2) -> is_part (rcons s sn.+1).
proof: Proof. elim: s => //= s0 s IHs. move => /andP[Hhead {}/IHs ->]; rewrite andbT. case: s Hhead => [| s1 s]; first exact: ltn_trans. by rewrite !rcons_cons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition