proposition: Lemma nthE T (def : T) s i : List.nth i s def = nth def s i.
proof: Proof. elim: s i => [|x s IHs i]; first by case. by case: i. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)