31 val nat_bound_opt : Nat.nat -> Nat.nat -> __ Types.option
34 | Nat_lt of Nat.nat * Nat.nat
36 | Nat_gt of Nat.nat * Nat.nat
38 val nat_compared_rect_Type4 :
39 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
40 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
42 val nat_compared_rect_Type5 :
43 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
44 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
46 val nat_compared_rect_Type3 :
47 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
48 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
50 val nat_compared_rect_Type2 :
51 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
52 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
54 val nat_compared_rect_Type1 :
55 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
56 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
58 val nat_compared_rect_Type0 :
59 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
60 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
62 val nat_compared_inv_rect_Type4 :
63 Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
64 -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
65 -> __ -> __ -> 'a1) -> 'a1
67 val nat_compared_inv_rect_Type3 :
68 Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
69 -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
70 -> __ -> __ -> 'a1) -> 'a1
72 val nat_compared_inv_rect_Type2 :
73 Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
74 -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
75 -> __ -> __ -> 'a1) -> 'a1
77 val nat_compared_inv_rect_Type1 :
78 Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
79 -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
80 -> __ -> __ -> 'a1) -> 'a1
82 val nat_compared_inv_rect_Type0 :
83 Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
84 -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
85 -> __ -> __ -> 'a1) -> 'a1
87 val nat_compared_discr :
88 Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __
90 val nat_compared_jmdiscr :
91 Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __
93 val nat_compare : Nat.nat -> Nat.nat -> nat_compared
95 val eq_nat_dec : Nat.nat -> Nat.nat -> (__, __) Types.sum