proposition: Lemma nth_error_None l n : nth_error l n = None <-> length l <= n.
proof: Proof. revert n. induction l as [|? ? IHl]; intro n; destruct n; simpl. - split; auto. - now split; intros; [apply Nat.le_0_l|]. - now split; [|intros ? %Nat.nle_succ_0]. - now rewrite IHl, Nat.succ_le_mono. Qed.
imports: PeanoNat