stuck with chomp10s

minimal.v

Require Import Coq.PArith.BinPos.
Require Import Coq.NArith.BinNat.

Open Scope positive_scope.
Open Scope N_scope.

Fixpoint chomp10s (p : positive) : N :=
  match p with
  | p'~1~0 => chomp10s p'
  | 1~0 => N0
  | _ => Npos p
  end.

Definition ends_with_10 (n : N) : Prop :=
  match n with
  | N0 => False
  | Npos p =>
    match p with
    | p'~1~0 => True
    | 1~0 => True
    | _ => False
    end
  end.

Theorem chomp10s_correct : forall p : positive, ~ ends_with_10 (chomp10s p).
Proof.
  unfold not.
  induction p.
  - contradiction.
  - intros.
Abort.