feat(Algebra/Order/Floor/Defs): add instances on FloorSemiring and FloorRing (#36828)

These instances are `NeZero` and `Nontrivial` instances, made so that we can weaken the `IsStrictOrderedRing` instances on several theorems about floor rings into `IsOrderedRing`.

Author: mortarsanjaya

Mathlib/Algebra/Order/Floor/Defs.lean

@@ -123,6 +123,12 @@ theorem gc_ceil_coe : GaloisConnection (ceil : α → ℕ) (↑) :=
 theorem ceil_le : ⌈a⌉₊ ≤ n ↔ a ≤ n :=
   gc_ceil_coe _ _
 
+instance : NeZero (1 : α) :=
+  ⟨fun h ↦ not_succ_le_self ⌊(0 : α)⌋₊ <|
+    (le_floor_iff (le_refl 0)).mpr (eq_zero_of_zero_eq_one h.symm _).le⟩
+
+instance : Nontrivial α := NeZero.nontrivial 1
+
 end OrderedSemiring
 
 section LinearOrderedSemiring
@@ -256,6 +262,12 @@ theorem floorRing_floor_eq : @FloorRing.floor = @Int.floor :=
 theorem floorRing_ceil_eq : @FloorRing.ceil = @Int.ceil :=
   rfl
 
+instance : NeZero (1 : α) :=
+  ⟨fun h ↦ (Int.lt_succ ⌊(0 : α)⌋).not_ge <|
+    (FloorRing.gc_coe_floor _ _).mp (eq_zero_of_zero_eq_one h.symm _).le⟩
+
+instance : Nontrivial α := NeZero.nontrivial 1
+
 /-! #### Floor -/
 
 theorem gc_coe_floor : GaloisConnection ((↑) : ℤ → α) floor :=

Mathlib/Logic/Nontrivial/Defs.lean

@@ -131,3 +131,6 @@ instance : Nontrivial Bool :=
   ⟨⟨true, false, nofun⟩⟩
 
 end Bool
+
+theorem NeZero.nontrivial {α : Type*} [Zero α] (a : α) [NeZero a] : Nontrivial α :=
+  ⟨⟨a, 0, NeZero.ne a⟩⟩