proposition: Lemma nth_cons (a x : A) (s : seq A) (n : nat) : nth a (x :: s) n = if n == 0 then x else nth a s n.-1.
proof: Proof. by case: n. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)