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 (**************************************************************************)
15 include "Ground_2/arith.ma".
17 (* TRICOTOMY FUNCTION *******************************************************)
19 let rec tri (A:Type[0]) m n a b c on m : A ≝
21 [ O ⇒ match n with [ O ⇒ b | S n ⇒ a ]
22 | S m ⇒ match n with [ O ⇒ c | S n ⇒ tri A m n a b c ]
25 (* Basic properties *********************************************************)
27 lemma tri_lt: ∀A,a,b,c,n,m. m < n → tri A m n a b c = a.
28 #A #a #b #c #n elim n -n
29 [ #m #H elim (lt_zero_false … H)
30 | #n #IH #m elim m -m // /3 width=1/
34 lemma tri_eq: ∀A,a,b,c,m. tri A m m a b c = b.
35 #A #a #b #c #m elim m -m normalize //
38 lemma tri_gt: ∀A,a,b,c,m,n. n < m → tri A m n a b c = c.
39 #A #a #b #c #m elim m -m
40 [ #n #H elim (lt_zero_false … H)
41 | #m #IH #n elim n -n // /3 width=1/