victory.v

Require Import NArith ZArith PArith.

Ltac is_positive p :=
  lazymatch p with
  | xI ?pa => is_positive pa
  | xO ?pa => is_positive pa
  | xH => idtac
  | _ => fail
  end.
Ltac is_N n :=
  lazymatch n with
  | N0 => idtac
  | Npos ?p => is_positive p
  | _ => fail
  end.

Open Scope N_scope.
(* Ltac is_N n := match n with | N0 => idtac | Npos ?p => is_positive p | _ => fail "Not constant" end. *)
Goal forall n : N, (42 + 13) + (n + 7) + (n + n) = 62 + 3 * n.
intros.
(* let n := constr:(0%N) in
let c := is_N n in idtac c. *)
match goal with
  | |- context [?n + ?p] =>
  idtac "n" n;
  is_N n;
  idtac "p" p
  (* idtac res "n" n "p" p; *)
  | _ => idtac "done"
end.

output:

n (42 + 13 + (n + 7))
n (42 + 13)
n 42
p 13