proposition: Lemma nth_rcons_default s i : nth (rcons s x0) i = nth s i.
proof: Proof. by rewrite nth_rcons; case: ltngtP => //[/ltnW ?|->]; rewrite nth_default. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)