intros n m. generalize dependent n.

Require Import ListTactics.

Ltac introNthAcc n acc := match constr:n with
  | 0    => intro ; list_iter ltac:(fun x => generalize dependent x) acc
  | S ?n =>
     let H := fresh "H" in
     intro H ; introNthAcc n (cons H acc)
end.

Ltac introNth n := introNthAcc n (@nil Prop).

Goal forall a b c, a / b / c.

 introNth 1.

intros n m. generalize dependent n.

move=> n m; move: n.

Lemma my_lemma n m : P n m.
Proof.
move: n.
(* Rest of proof *)
Qed.

Lemma my_lemma n m : P n m.
Proof.
elim: n.
(* Rest of proof *)
Qed.