[Merged by Bors] - feat(algebra/ordered_monoid): min_*_distrib

src/algebra/ordered_monoid.lean

@@ -676,6 +676,26 @@ instance canonically_linear_ordered_monoid.semilattice_sup_bot
   [canonically_linear_ordered_monoid α] : semilattice_sup_bot α :=
 { ..lattice_of_linear_order, ..canonically_ordered_monoid.to_order_bot α }
 
+instance with_top.canonically_linear_ordered_add_monoid
+  (α : Type*) [canonically_linear_ordered_add_monoid α] :
+    canonically_linear_ordered_add_monoid (with_top α) :=
+{ .. (infer_instance : canonically_ordered_add_monoid (with_top α)),
+  .. (infer_instance : linear_order (with_top α)) }
+
+@[to_additive] lemma min_mul_distrib [canonically_linear_ordered_monoid α] (a b c : α) :
+  min a (b * c) = min a (min a b * min a c) :=
+begin
+  cases le_total a b with hb hb,
+  { simp [hb, le_mul_right] },
+  { cases le_total a c with hc hc,
+    { simp [hc, le_mul_left] },
+    { simp [hb, hc] } }
+end
+
+@[to_additive] lemma min_mul_distrib' [canonically_linear_ordered_monoid α] (a b c : α) :
+  min (a * b) c = min (min a c * min b c) c :=
+by simpa [min_comm _ c] using min_mul_distrib c a b
+
 end canonically_linear_ordered_monoid
 
 /-- An ordered cancellative additive commutative monoid

src/data/nat/basic.lean

@@ -94,6 +94,10 @@ instance : canonically_ordered_comm_semiring ℕ :=
   .. (infer_instance : linear_ordered_semiring ℕ),
   .. (infer_instance : comm_semiring ℕ) }
 
+instance : canonically_linear_ordered_add_monoid ℕ :=
+{ .. (infer_instance : canonically_ordered_add_monoid ℕ),
+  .. nat.linear_order }
+
 instance nat.subtype.semilattice_sup_bot (s : set ℕ) [decidable_pred s] [h : nonempty s] :
   semilattice_sup_bot s :=
 { bot := ⟨nat.find (nonempty_subtype.1 h), nat.find_spec (nonempty_subtype.1 h)⟩,

src/data/real/nnreal.lean

@@ -228,6 +228,10 @@ instance : canonically_ordered_add_monoid ℝ≥0 :=
   ..nnreal.order_bot,
   ..nnreal.linear_order }
 
+instance : canonically_linear_ordered_add_monoid ℝ≥0 :=
+{ .. (infer_instance : canonically_ordered_add_monoid ℝ≥0),
+  .. nnreal.linear_order }
+
 instance : distrib_lattice ℝ≥0 := by apply_instance
 
 instance : semilattice_inf_bot ℝ≥0 :=

src/set_theory/cardinal.lean

@@ -275,6 +275,10 @@ instance : canonically_ordered_comm_semiring cardinal.{u} :=
   ..cardinal.order_bot,
   ..cardinal.comm_semiring, ..cardinal.linear_order }
 
+noncomputable instance : canonically_linear_ordered_add_monoid cardinal.{u} :=
+{ .. (infer_instance : canonically_ordered_add_monoid cardinal.{u}),
+  .. cardinal.linear_order }
+
 @[simp] theorem zero_lt_one : (0 : cardinal) < 1 :=
 lt_of_le_of_ne (zero_le _) zero_ne_one