- ZERO_eq_neg_ZERO_thm
-
⊢ intOrd (&ZERO) (-&ZERO) = Equal
- pos_pos_thm
-
⊢ ∀m n. intOrd (&m) (&n) = numOrd m n
- neg_ZERO_eq_ZERO_thm
-
⊢ intOrd (-&ZERO) (&ZERO) = Equal
- neg_neg_thm
-
⊢ ∀m n. intOrd (-&m) (-&n) = numOrd n m
- neg_lt_BIT2_thm
-
⊢ ∀m n. intOrd (-&m) (&BIT2 n) = Less
- neg_lt_BIT1_thm
-
⊢ ∀m n. intOrd (-&m) (&BIT1 n) = Less
- neg_BIT2_lt_thm
-
⊢ ∀m n. intOrd (-&BIT2 m) (&n) = Less
- neg_BIT1_lt_thm
-
⊢ ∀m n. intOrd (-&BIT1 m) (&n) = Less
- gt_neg_BIT2_thm
-
⊢ ∀m n. intOrd (&m) (-&BIT2 n) = Greater
- gt_neg_BIT1_thm
-
⊢ ∀m n. intOrd (&m) (-&BIT1 n) = Greater
- BIT2_nz
-
⊢ ∀n. BIT2 n ≠ 0
- BIT2_gt_neg_thm
-
⊢ ∀m n. intOrd (&BIT2 m) (-&n) = Greater
- BIT1_nz
-
⊢ ∀n. BIT1 n ≠ 0
- BIT1_gt_neg_thm
-
⊢ ∀m n. intOrd (&BIT1 m) (-&n) = Greater
- apintto_thm
-
⊢ apto intto = intOrd