proposition: Lemma In_nth_exists {A} (l: list A) x def : List.In x l -> exists n, nth def l n = x /\ (n < length l)%coq_nat.
proof: Proof. elim : l => [| a l IHl] //=. move => [H | /IHl [n [H1 H2]]]; subst. exists 0; split => //; lia. exists n.+1; split => //; lia. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)