feat(library/init/algebra): add zero_ne_one and one_ne_zero to default simp-set

library/init/algebra/field.lean

@@ -75,8 +75,8 @@ have 0 = (1:α), from eq.symm (by rw [-(mul_one_div_cancel h), this, mul_zero]),
 absurd this zero_ne_one
 
 lemma one_inv_eq : 1⁻¹ = (1:α) :=
-suffices 1 * 1⁻¹ = (1:α), begin simp at this, assumption end,
-mul_inv_cancel (ne.symm (@zero_ne_one α _))
+calc 1⁻¹ = 1 * 1⁻¹ : by rw [one_mul]
+     ... = (1:α)   : by simp
 
 local attribute [simp] one_inv_eq
 

library/init/algebra/ring.lean

@@ -41,9 +41,14 @@ mul_zero_class.mul_zero a
 class zero_ne_one_class (α : Type u) extends has_zero α, has_one α :=
 (zero_ne_one : 0 ≠ (1:α))
 
+@[simp]
 lemma zero_ne_one [s: zero_ne_one_class α] : 0 ≠ (1:α) :=
 @zero_ne_one_class.zero_ne_one α s
 
+@[simp]
+lemma one_ne_zero [s: zero_ne_one_class α] : (1:α) ≠ 0 :=
+take h, @zero_ne_one_class.zero_ne_one α s h^.symm
+
 /- semiring -/
 
 class semiring (α : Type u) extends add_comm_monoid α, monoid α, distrib α, mul_zero_class α