Coq induction start at specific nat

Question

I'm trying to learn coq so please assume I know nothing about it. If I have a lemma in coq that starts ``` forall n m:nat, n>=1 -> m>=1 ... ``` And I want to proceed by induction on n. How do I start the induction at 1? Currently when I use the "induction n." tactic it starts at zero and this makes the base statement false which makes it hard to proceed. Any hints?

Accepted Answer

The following is a proof that every proposition `P` is true forall `n>=1`, if `P` is true for `1` and if `P` is inductively true.

```
Require Import Omega.

Parameter P : nat -> Prop.
Parameter p1 : P 1.
Parameter pS : forall n, P n -> P (S n).

Goal forall n, n>=1 -> P n.
```

We begin the proof by induction.

```
  induction n; intro.
```

A false base case is no problem, if you have a false hypothesis laying around. In this case `0>=1`.

```
  - exfalso. omega.
```

The inductive case is tricky, because to access a proof of `P n`, we first have to proof that `n>=1`. The trick is to do a case analysis on `n`. If `n=0`, then we can trivially proof the goal `P 1`. If `n>=1`, we can access `P n`, and then proof the rest.

```
  - destruct n.
    + apply p1.
    + assert (S n >= 1) by omega.
      intuition.
      apply pS.
      trivial.
Qed.
```

Coq induction start at specific nat

Solution

Problem