proposition: Theorem index_correct4 : forall (n : nat) (s : string), index n EmptyString s = None -> length s < n.
proof: Proof. intros n s; generalize n; clear n; elim s; simpl; auto. - intros n; case n; simpl; auto. + intros; discriminate. + intros; apply Nat.lt_0_succ. - intros a s' H n; case n; simpl; auto. + intros; discriminate. + intros n'; generalize (H n'); case (index n' EmptyString s'); simpl; auto. * intros; discriminate. * intros H0 H1. apply -> Nat.succ_lt_mono; auto. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte