proposition: Lemma nth_error_Some l n : nth_error l n <> None <-> n < length l.
proof: Proof. revert n. induction l as [|? ? IHl]; intro n; destruct n; simpl. - split; [now destruct 1 | inversion 1]. - split; [now destruct 1 | inversion 1]. - now split; intros; [apply Nat.lt_0_succ|]. - now rewrite IHl, Nat.succ_lt_mono. Qed.
imports: PeanoNat