--- 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)