coq - COQ での 2 つの再帰関数の展開を含む証明

Question

私は Coq の学習を開始し、かなり単純に見えることを証明しようとしています: リストに x が含まれている場合、そのリスト内の x のインスタンスの数は > 0 になります。

次のように、contains 関数と count 関数を定義しました。

Fixpoint contains (n: nat) (l: list nat) : Prop :=
  match l with
  | nil => False
  | h :: t => if beq_nat h n then True else contains n t
  end.

Fixpoint count (n acc: nat) (l: list nat) : nat :=
  match l with
  | nil => acc
  | h :: t => if beq_nat h n then count n (acc + 1) t else count n acc t
  end.

私は証明しようとしています：

Lemma contains_count_ge1 : forall (n: nat) (l: list nat), contains n l -> (count n 0 l > 0).

証明にはcountとcontainsの定義を展開することが含まれることを理解していますが、「containsがtrueであるため、リストをnilにすることはできません。そのため、trueである要素が存在する必要があります」と言いたいxです。少し遊んでみましたが、戦術を使ってこれを行う方法がわかりません。ガイダンスをいただければ幸いです。lbeq_nat h x