chore(algebra/order/group): Restore basic instances (#17810)

Moving the inheritance instances results in unexpected and confusing errors when importing `algebra.order.group.defs` but not `algebra.order.group.instances`. This puts the inheritance instances back into `algebra.order.group.defs`.

src/algebra/order/group/defs.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import order.hom.basic
 import algebra.order.sub.defs
-import algebra.order.monoid.defs
+import algebra.order.monoid.cancel.defs
 
 /-!
 # Ordered groups
@@ -47,6 +47,12 @@ instance ordered_comm_group.to_covariant_class_left_le (α : Type u) [ordered_co
   covariant_class α α (*) (≤) :=
 { elim := λ a b c bc, ordered_comm_group.mul_le_mul_left b c bc a }
 
+@[priority 100, to_additive] -- See note [lower instance priority]
+instance ordered_comm_group.to_ordered_cancel_comm_monoid [ordered_comm_group α] :
+  ordered_cancel_comm_monoid α :=
+{ le_of_mul_le_mul_left := λ a b c, le_of_mul_le_mul_left',
+  ..‹ordered_comm_group α› }
+
 example (α : Type u) [ordered_add_comm_group α] : covariant_class α α (swap (+)) (<) :=
 add_right_cancel_semigroup.covariant_swap_add_lt_of_covariant_swap_add_le α
 
@@ -807,6 +813,11 @@ instance linear_ordered_comm_group.to_no_min_order [nontrivial α] : no_min_orde
     exact λ a, ⟨a / y, (div_lt_self_iff a).mpr hy⟩
   end ⟩
 
+@[priority 100, to_additive] -- See note [lower instance priority]
+instance linear_ordered_comm_group.to_linear_ordered_cancel_comm_monoid :
+  linear_ordered_cancel_comm_monoid α :=
+{ ..‹linear_ordered_comm_group α›, ..ordered_comm_group.to_ordered_cancel_comm_monoid }
+
 end linear_ordered_comm_group
 
 namespace add_comm_group

src/algebra/order/group/instances.lean

@@ -17,21 +17,9 @@ import algebra.order.monoid.order_dual
 
 variables {α : Type*}
 
-@[priority 100, to_additive]    -- see Note [lower instance priority]
-instance ordered_comm_group.to_ordered_cancel_comm_monoid [s : ordered_comm_group α] :
-  ordered_cancel_comm_monoid α :=
-{ le_of_mul_le_mul_left := λ a b c, (mul_le_mul_iff_left a).mp,
-  ..s }
-
 @[to_additive] instance [ordered_comm_group α] : ordered_comm_group αᵒᵈ :=
 { .. order_dual.ordered_comm_monoid, .. order_dual.group }
 
 @[to_additive] instance [linear_ordered_comm_group α] :
   linear_ordered_comm_group αᵒᵈ :=
 { .. order_dual.ordered_comm_group, .. order_dual.linear_order α }
-
-@[priority 100, to_additive] -- see Note [lower instance priority]
-instance linear_ordered_comm_group.to_linear_ordered_cancel_comm_monoid
-  [linear_ordered_comm_group α] : linear_ordered_cancel_comm_monoid α :=
-{ le_of_mul_le_mul_left := λ x y z, le_of_mul_le_mul_left',
-  ..‹linear_ordered_comm_group α› }