# How to prove a statement about sublists?

I create sublist from list in this way:

Fixpoint sublist {X : Type} (n : nat) (m : nat) (lst : list X) : list X :=
match lst with
| [] => []
| h :: t => match m with
| O => match n with
| O => []
| S n' => h :: sublist n' O t
end

| S m' => sublist n m' t
end
end.


I want to prove that if m is greater or equal to the length of lst, then sublist n m lst will return empty list:

Theorem sublist_list_after_m :  forall X : Type, forall n m : nat, forall lst :list X ,
m <? (length lst) = false -> length (sublist n m lst) =? 0 = true.
Proof.
intros.
destruct lst as [|h t].
- simpl. reflexivity.
- simpl. destruct n as [|n'].
+ simpl. reflexivity.
+ destruct m as [|m'].


But I not sure what I'm doing wrong.

• What is this for? Homework for a class? Something else? You'll need to use induction here. Try starting your proof with induction m as [ | m IHm].
– djao
Apr 12 at 13:14

as @djao said, you need to use induction.

Below you will find one possible proof for your Theorem (without ssreflect). The strategy is essentially induction on lst (note the generalized H and m to strengthen de induction hypothesis).

Theorem sublist_list_after_m :  forall X : Type, forall n m : nat, forall lst :list X ,
m <? (length lst) = false -> length (sublist n m lst) =? 0 = true.
Proof.
intros X n m lst H; revert H; generalize m.
induction lst; [ simpl; reflexivity | ].

intros; simpl.
destruct m0; [ discriminate | ].
specialize (IHlst m0).

apply IHlst, Nat.ltb_ge; apply Nat.ltb_ge in H.
simpl in H; apply le_S_n in H.

exact H.
Qed.
$$$$
`