# HG changeset patch
# User haftmann
# Date 1617810366 0
# Node ID fc72e5ebf9de4e1537cefe98206a1272ac0ff7a3
# Parent  79761915770c94b4c0fcd36c686e9c505d347ca0
subclass relation

diff -r 79761915770c -r fc72e5ebf9de src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Apr 07 22:32:43 2021 +0200
+++ b/src/HOL/Rings.thy	Wed Apr 07 15:46:06 2021 +0000
@@ -1933,6 +1933,15 @@
 
 class zero_less_one = order + zero + one +
   assumes zero_less_one [simp]: "0 < 1"
+begin
+
+subclass zero_neq_one
+  by standard (simp add: less_imp_neq)
+
+lemma zero_le_one [simp]:
+  \<open>0 \<le> 1\<close> by (rule less_imp_le) simp
+
+end
 
 class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one
 begin