forall n p : nat, n <= p -> p < S n -> n = p. forall n : nat, 2 * n < 2 -> n = 0. forall n p : nat , forall n p : nat, p < n -> 3 * n <> 2 * p.