# HG changeset patch
# User nipkow
# Date 1589492641 -7200
# Node ID f4626b1f1b9689e1bd9531be7fd45587c10473bf
# Parent  8ed78bb0b915f6e934a37edbe7ccc1e120dbd39d
added lemma

diff -r 8ed78bb0b915 -r f4626b1f1b96 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu May 14 13:44:44 2020 +0200
+++ b/src/HOL/Nat.thy	Thu May 14 23:44:01 2020 +0200
@@ -900,6 +900,9 @@
 lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
   by (simp split: nat.split)
 
+lemma max_0_iff[simp]: "max m n = (0::nat) \<longleftrightarrow> m = 0 \<and> n = 0"
+by(cases m, auto simp: max_Suc1 split: nat.split)
+
 lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)"
   for m n q :: nat
   by (simp add: min_def not_le)