Show that with_one is an ordered commutative monoid

OrderedSemigroups/SemigroupToMonoid.lean

@@ -57,18 +57,18 @@ end CommSemigroup'
 section LinearOrderedCancelSemigroup
 variable [LinearOrderedCancelCommSemigroup α]
 
-instance : OrderedCommMonoid (with_one α) where
+instance (not_one : ∀x : α, ¬is_one x): OrderedCommMonoid (with_one α) where
   le := by
     intro x y
-    rcases x with x | one
-    <;> rcases y with y | one
+    rcases x with x | _
+    <;> rcases y with y | _
     · exact x ≤ y
     · exact x*x ≤ x
     · exact y*y ≥ y
     · exact True
   le_refl := by
     intro x
-    rcases x with x | one
+    rcases x with x | _
     <;> simp
   le_trans := by
     intro x y z x_le_y y_le_z
@@ -90,10 +90,21 @@ instance : OrderedCommMonoid (with_one α) where
     <;> rcases y with y | one
     <;> simp at *
     · rw [PartialOrder.le_antisymm x y x_le_y y_le_x]
-    · sorry
-    · sorry
-  mul_le_mul_left := sorry
-
+    · exact not_one x (one_right_one_forall (PartialOrder.le_antisymm (x*x) x x_le_y y_le_x))
+    · exact not_one y (one_right_one_forall (PartialOrder.le_antisymm (y*y) y y_le_x x_le_y))
+  mul_le_mul_left := by
+    intro x y x_le_y z
+    rcases x with x | one
+    <;> rcases y with y | one
+    <;> rcases z with z | one
+    <;> unfold_projs
+    <;> simp at *
+    · exact mul_le_mul_left' x_le_y z
+    · trivial
+    · exact not_pos_right (not_pos_iff.mpr x_le_y) z
+    · exact x_le_y
+    · exact not_neg_right (not_neg_iff.mpr x_le_y) z
+    · trivial
 
 
 

OrderedSemigroups/Sign.lean

@@ -297,4 +297,29 @@ theorem not_pos_le_not_neg {a b : α} (not_pos : ¬is_positive a) (not_neg : ¬i
   · exact (one_lt_pos one_a pos_b).le
   · exact (one_unique one_a one_b).le
 
+theorem not_positive {a : α} (not_pos : ¬is_positive a) : ∀x : α, a * x ≤ x := by
+  intro x
+  obtain neg_a | one_a := not_pos_or not_pos
+  · exact le_of_lt (neg_a x)
+  · exact le_of_eq (one_a x)
+
+theorem not_pos_right {a : α} (not_pos : ¬is_positive a) : ∀x : α, x * a ≤ x := by
+  intro x
+  obtain neg_a | one_a := not_pos_or not_pos
+  · exact le_of_lt (neg_right neg_a x)
+  · exact le_of_eq (one_right one_a x)
+
+
+theorem not_negative {a : α} (not_neg : ¬is_negative a) : ∀x : α, a * x ≥ x := by
+  intro x
+  obtain pos_a | one_a := not_neg_or not_neg
+  · exact le_of_lt (pos_a x)
+  · exact Eq.ge (one_a x)
+
+theorem not_neg_right {a : α} (not_neg : ¬is_negative a) : ∀x : α, x * a ≥ x := by
+  intro x
+  obtain pos_a | one_a := not_neg_or not_neg
+  · exact le_of_lt (pos_right pos_a x)
+  · exact le_of_eq (one_right one_a x).symm
+
 end LinearOrderedCancelSemigroup