proposition: Theorem substring_correct2 : forall (s : string) (n m p : nat), m <= p -> get p (substring n m s) = None.
proof: Proof. intros s; elim s; simpl; auto. - intros n; case n; simpl; auto. intros m; case m; simpl; auto. - intros a s' Rec; intros n; case n; simpl; auto. intros m; case m; simpl; auto. intros m' p; case p; simpl; auto. + intros H; inversion H. + intros n0 H; apply Rec; simpl; auto. apply <- Nat.succ_le_mono; auto. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte