From ab404beb01ca3352045529d1ddfd9d5a135bd7da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Aug 2014 21:51:41 -0700 Subject: [PATCH] chore(library/standard/data/nat/order): remove unnecessary 'proofs' Signed-off-by: Leonardo de Moura --- library/standard/data/nat/order.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/library/standard/data/nat/order.lean b/library/standard/data/nat/order.lean index 831bdf1ea..69589b4ec 100644 --- a/library/standard/data/nat/order.lean +++ b/library/standard/data/nat/order.lean @@ -436,14 +436,10 @@ resolve_left (le_or_gt m n) H theorem not_le_imp_gt {n m : ℕ} (H : ¬ n ≤ m) : n > m := resolve_right (le_or_gt n m) H -theorem lt_decidable [instance] (n m : ℕ) : decidable (n < m) := -le_decidable _ _ - -theorem gt_decidable [instance] (n m : ℕ) : decidable (n > m) := -le_decidable _ _ - -theorem ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m) := -le_decidable _ _ +-- The following three theorems are automatically proved using the instance le_decidable +theorem lt_decidable [instance] (n m : ℕ) : decidable (n < m) +theorem gt_decidable [instance] (n m : ℕ) : decidable (n > m) +theorem ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m) -- Note: interaction with multiplication under "positivity"