subclass relation
authorhaftmann
Wed, 07 Apr 2021 15:46:06 +0000
changeset 73801 fc72e5ebf9de
parent 73800 79761915770c
child 73802 7cb3fefef79e
child 73803 a7aabdf889b7
subclass relation
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