proposition: Lemma nth_rcons s x n : nth (rcons s x) n = if n < size s then nth s n else if n == size s then x else x0.
proof: Proof. by elim: s n => [|y s IHs] [] //=; apply: nth_nil. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)