Well-founded induction for a counting predicate

Question

Here is the definition for the Count predicate. It uses 2 indices to denote starting and ending elements, "check" predicate to count/skip the "current" element and the last argument "sum" to keep track the number of elements that satisfy check predicate between these boundary indices.

Require Import ZArith.

Open Scope Z_scope.

Inductive Count : Z -> Z -> (Z -> Prop) -> Z -> Prop :=
    | Q_Nil:
        forall (m n : Z),
        forall (check : Z -> Prop),
          (n <= m) ->
            (Count m n check 0)
    | Q_Hit:
        forall (m n sum : Z),
        forall (check : Z -> Prop),
          let x := (n - 1) in
            (m < n) ->
            (check x) ->
            (Count m x check sum) ->
              (Count m n check (1 + sum))
    | Q_Miss:
        forall (m n sum : Z),
        forall (check : Z -> Prop),
          let x := (n - 1) in
            (m < n) ->
            ~(check x) ->
            (Count m x check sum) ->
              (Count m n check sum).

It is required to prove that the number of counted elements "sum" is non-negative.

Goal
  forall (m n sum : Z),
  forall (check : Z -> Prop),
    (Count m n check sum) -> (0 <= sum).
Proof.

Obviously, the induction could be applied here. However, schemes like natlike_rec3 are not applicable because of the Q_Hit|Q_Miss difference in sum element (i.e. +1 in Q_Hit).

Here is my proof attempt till the step where an induction should be applied.

Proof.
Require Import Psatz.
intros m n sum check.
assert (X: n <= m \/ n > m) by lia.
destruct X as [le|gt].
+ intro.
  inversion H; subst; intuition.
+ pose (p := (n - m)).
  assert (PZ: p > 0). { subst p. auto with zarith. }
  replace n with (m + p) in * by (subst p; auto with zarith).

1 subgoal
m, n, sum : Z
check : Z -> Prop
p := n - m : Z
gt : m + p > m
PZ : p > 0
______________________________________(1/1)
Count m (m + p) check sum -> 0 <= sum

I think that maybe well_founded_induction_type_2 could be used further with relation on sum and p: sum <= p.

Answer 1

You can use induction on the Count hypothesis (in a way, that's the main point of Inductive types).

Proof.
  intros.
  induction H.
  all: omega.
  (* or, as a single sequence: intros; induction H; omega. *)
  (* lia also works instead of omega, and should probably be preferred nowadays (Require Import Lia.) *)
Qed.