Using maximal induction principles (le)

Use the Scheme command to generate the maximal induction principle for le.

The following text defines a function with a pre-condition based on le and proves a small theorem about this function.

Definition pred_partial: forall (n : nat), n <> 0 ->  nat.
intros n; case n.
intros h; elim h; reflexivity.
intros p h'; exact p.
Defined.

Theorem le_2_n_not_zero: forall (n : nat), 2 <= n ->  (n <> 0).
Proof.
intros n Hle; elim Hle; intros; discriminate.
Qed.

Prove the following theorem, using the maximal induction principle.

Theorem le_2_n_pred:
 forall (n : nat) (h : 2 <= n),  (pred_partial n (le_2_n_not_zero n h) <> 0).

Solution

Look at this file


Going home
Pierre Castéran