From c2fc612ec120dffb44d0f8763683b5efc8227cab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Jul 2015 20:21:25 -0700 Subject: [PATCH] fix(library/data/nat/order): add missing theorems back --- library/data/nat/order.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 19b41522f..abdbc3c23 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -537,6 +537,13 @@ decidable.by_cases theorem max_add_add_right (a b c : ℕ) : max (a + c) (b + c) = max a b + c := by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply max_add_add_left +theorem max_eq_right' {a b : ℕ} (H : a < b) : max a b = b := +if_pos H + +-- different versions will be defined in algebra +theorem max_eq_left' {a b : ℕ} (H : ¬ a < b) : max a b = a := +if_neg H + /- greatest -/ section greatest