From dbb3b7c72a887656122a4018719aecc6eda027ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Nov 2014 17:56:42 -0800 Subject: [PATCH] refactor(library/data/nat/sub): cleanup 'max' theorems --- library/data/nat/sub.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 307659b4f..2db4608e7 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -368,13 +368,17 @@ sub_split definition max (n m : ℕ) : ℕ := n + (m - n) definition min (n m : ℕ) : ℕ := m - (m - n) -theorem max_le {n m : ℕ} (H : n ≤ m) : n + (m - n) = m := add_sub_le H +theorem max_le {n m : ℕ} (H : n ≤ m) : max n m = m := +add_sub_le H -theorem max_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n := add_sub_ge H +theorem max_ge {n m : ℕ} (H : n ≥ m) : max n m = n := +add_sub_ge H -theorem left_le_max (n m : ℕ) : n ≤ n + (m - n) := !le_add_sub_left +theorem left_le_max (n m : ℕ) : n ≤ max n m := +!le_add_sub_left -theorem right_le_max (n m : ℕ) : m ≤ max n m := !le_add_sub_right +theorem right_le_max (n m : ℕ) : m ≤ max n m := +!le_add_sub_right -- ### absolute difference