Proof with forall for a particular term

If your proof has a name, for example:

Lemma My_PropertyP : forall (n : nat), 0 <= n -> My_Property n.

you can refer to the case n = 2 with My_PropertyP 2:

Check (My_PropertyP 2).
(*
My_PropertyP 2
     : 0 <= 2 -> My_Property 2
*)

And since indeed we can prove 0 <= 2,

Lemma leq_0_2 : 0 <= 2. Proof. auto. Qed.

we can even instantiate this proof to obtain My_Property 2:

Check (My_PropertyP 2 leq_0_2).
(*
My_PropertyP 2 leq_0_2
     : My_Property 2
*)

The above illustrates that you can think of lemmas as functions. name : forall (n : nat), P n represents a function called name that receives an element n of type nat and outputs an element of type P n. If P n has type Prop we usually say that name is a "lemma" instead of a "function" and that name n is a "proof of P n" instead of an "element of type P n", but ultimately they are just different names for the same thing. This is related to the Curry-Howard Isomorphism.

P.S. 0 <= n holds for every natural number, so it is spurious in this particular example.

If your goal is to prove that for every n something holds, then showing the particular case n = 2 won't solve the goal.

If you want to give a different proof for n = 2 than for every other n, you have two options:

1. Case analysis on n.

  intro n.
  case n.
  - admit. (* 0 *)
  - intro n'; case n'.
    + admit. (* 1 *)
    + intro n''; case n''.
      * admit. (* 2 *)
      * admit. (* 3 <= n *)

2. Case analysis on whether n equals 2.

Require Import Arith.
(*...*)
intro n.
case (Nat.eq_dec n 2).
- (* n = 2 -> ... *)
  admit.
- (* n <> 2 -> ... *)
  admit.