3 (function n -> (function m ->
7 Matita_nat_nat.O -> Matita_datatypes_bool.True
8 | Matita_nat_nat.S(q) -> Matita_datatypes_bool.False)
10 | Matita_nat_nat.S(p) ->
12 Matita_nat_nat.O -> Matita_datatypes_bool.False
13 | Matita_nat_nat.S(q) -> (eqb p q))
20 (function n -> (function m ->
22 Matita_nat_nat.O -> Matita_datatypes_bool.True
23 | Matita_nat_nat.S(p) ->
25 Matita_nat_nat.O -> Matita_datatypes_bool.False
26 | Matita_nat_nat.S(q) -> (leb p q))
32 (function n -> (function m -> (Matita_datatypes_bool.andb (leb n m) (Matita_datatypes_bool.notb (eqb n m)))))
37 (function n -> (function m ->
41 Matita_nat_nat.O -> Matita_datatypes_compare.EQ
42 | Matita_nat_nat.S(q) -> Matita_datatypes_compare.LT)
44 | Matita_nat_nat.S(p) ->
46 Matita_nat_nat.O -> Matita_datatypes_compare.GT
47 | Matita_nat_nat.S(q) -> (nat_compare p q))