ch7_tactics_automation/le_lt_S_eq.html

<html>
<title> Using omega  </title>
<body>
<h1> Using omega </h1>

Prove the following theorems:
<pre>
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.
</pre>

<h2>Solution</h2>

Look at <a href="SRC/le_lt_S_eq.v"> this file </a>
<br>
<br>
<hr>

<hr>
</body>
</html>