1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 ninductive le (n: nat) : nat → CProp[0] ≝
19 | le_S: ∀m. le n m → le n (S m).
21 ndefinition lt ≝ λn,m. le (S n) m.
23 nlemma le_O_n: ∀n. le O n.
24 #n; nelim n [ napply le_n | #n'; #H; napply le_S; nassumption ]
28 naxiom le_S_S: ∀n,m. le n m → le (S n) (S m).
29 naxiom le_S_S_to_le: ∀n,m. le (S n) (S m) → le n m.
30 naxiom lt_Sn_m: ∀n,m. lt (S n) m → lt n m.
31 naxiom lt_to_le: ∀n,m. lt n m → le n m.
32 naxiom lt_le_trans: ∀n,m,p. lt n m → le m p → lt n p.
34 nlemma lt_O_Sn: ∀n. lt O (S n).
35 #n; napply le_S_S; napply le_O_n.