proposition: Lemma nth_imset T (def : T) l : nth def l @: [set n | n < length l] <--> l.
proof: Proof. case: l => [|x l] t; first by split=> //; case=> ?; rewrite ltn0; case. split; first by case=> n [? <-]; rewrite -nthE; apply/List.nth_In/ltP. by case/(In_nth_exists def) => n [? ?]; exists n; split=> //; apply/ltP. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)