Using omega

Prove the following theorem:

forall n p:nat, n <= p -> p < S n -> n = p.

Solution

Look at this file

Going home

Pierre Castéran