How to prove a statement about sublists?

Question

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'].
       -- Admitted. 

But I not sure what I'm doing wrong.

Answer 1

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.
```