proposition: Lemma nth_onth x0 n s : nth x0 s n = odflt x0 (onth s n).
proof: Proof. elim: s n=>/= [|a s IH] n /=; first by apply: nth_nil. by case: n. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)