diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index 68b5c5cfe..f14ac8f8b 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -19,7 +19,7 @@ definition absurd_a_lt_a {B : Type} {a : A} [s : strict_order A] (H : a < a) : B
 absurd H (lt.irrefl a)
 
 structure ordered_semiring [class] (A : Type)
-  extends semiring A, ordered_cancel_comm_monoid A, zero_ne_one_class A :=
+  extends semiring A, ordered_cancel_comm_monoid A :=
 (mul_le_mul_of_nonneg_left: ∀a b c, le a b → le zero c → le (mul c a) (mul c b))
 (mul_le_mul_of_nonneg_right: ∀a b c, le a b → le zero c → le (mul a c) (mul b c))
 (mul_lt_mul_of_pos_left: ∀a b c, lt a b → lt zero c → lt (mul c a) (mul c b))
@@ -100,13 +100,16 @@ section
 end
 
 structure linear_ordered_semiring [class] (A : Type)
-  extends ordered_semiring A, linear_strong_order_pair A
+  extends ordered_semiring A, linear_strong_order_pair A :=
+(zero_lt_one : lt zero one)
 
 section
   variable [s : linear_ordered_semiring A]
   variables {a b c : A}
   include s
 
+  theorem zero_lt_one : 0 < (1:A) := linear_ordered_semiring.zero_lt_one A
+
   theorem lt_of_mul_lt_mul_left (H : c * a < c * b) (Hc : c ≥ 0) : a < b :=
   lt_of_not_ge
     (assume H1 : b ≤ a,
@@ -378,7 +381,6 @@ section
     (assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H)
 
   theorem zero_le_one : 0 ≤ (1:A) := one_mul 1 ▸ mul_self_nonneg 1
-  theorem zero_lt_one : 0 < (1:A) := linear_ordered_ring.zero_lt_one A
 
   theorem pos_and_pos_or_neg_and_neg_of_mul_pos {a b : A} (Hab : a * b > 0) :
     (a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) :=
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 2636b47cd..1f2212ee9 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -165,7 +165,7 @@ section migrate_algebra
     add_lt_add_left            := @add_lt_add_left,
     add_le_add_left            := @add_le_add_left,
     le_of_add_le_add_left      := @le_of_add_le_add_left,
-    zero_ne_one                := ne.symm (succ_ne_zero zero),
+    zero_lt_one                := zero_lt_succ 0,
     mul_le_mul_of_nonneg_left  := (take a b c H1 H2, mul_le_mul_left c H1),
     mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right c H1),
     mul_lt_mul_of_pos_left     := @mul_lt_mul_of_pos_left,
@@ -223,7 +223,6 @@ section migrate_algebra
 end migrate_algebra
 
 theorem zero_le_one : 0 ≤ 1 := dec_trivial
-theorem zero_lt_one : 0 < 1 := dec_trivial
 
 /- properties specific to nat -/