## Stream: general

#### Johan Commelin (May 27 2020 at 08:32):

Is it ok if I move this to deprecated?

/--
If 0 is the least element in α, then with_zero α is an ordered_add_comm_monoid.
-/
(zero_le : ∀ a : α, 0 ≤ a) : ordered_add_comm_monoid (with_zero α) :=
begin
suffices, refine {
..with_zero.partial_order,
{ intros a b c h,
have h' := lt_iff_le_not_le.1 h,
rw lt_iff_le_not_le at ⊢,
refine ⟨λ b h₂, _, λ h₂, h'.2 $this _ _ h₂ _⟩, cases h₂, cases c with c, { cases h'.2 (this _ _ bot_le a) }, { refine ⟨_, rfl, _⟩, cases a with a, { exact with_bot.some_le_some.1 h'.1 }, { exact le_of_lt (lt_of_add_lt_add_left'$
with_bot.some_lt_some.1 h), } } },
{ intros a b h c ca h₂,
cases b with b,
{ rw le_antisymm h bot_le at h₂,
exact ⟨_, h₂, le_refl _⟩ },
cases a with a,
{ change c + 0 = some ca at h₂,
simp at h₂, simp [h₂],
{ simp at h,
cases c with c; change some _ = _ at h₂;
simp [-add_comm] at h₂; subst ca; refine ⟨_, rfl, _⟩,
{ exact h },
end


#### Johan Commelin (May 27 2020 at 08:33):

I'm pretty sure it's not used in mathlib, and I get the shivers by simply looking at the type of this def...

#### Gabriel Ebner (May 27 2020 at 08:42):

This looks perfectly reasonable to me. What is wrong with it?

#### Johan Commelin (May 27 2020 at 08:43):

Well, your type has a zero, and then you add a new zero to it. That's something that shouldn't be encouraged, I think.

#### Gabriel Ebner (May 27 2020 at 08:45):

Oh, I missed that. Then let's get rid of it!

#### Mario Carneiro (May 27 2020 at 09:11):

The point is to provide sufficient conditions on when with_zero A is an ordered_add_comm_monoid

#### Mario Carneiro (May 27 2020 at 09:13):

yes it's a weird theorem, but it's also a hole-filling theorem. I've said this before but we should have theorems about the pairwise interaction of all concepts in mathlib

#### Johan Commelin (May 27 2020 at 09:16):

Ok, I'll leave it there

Last updated: May 14 2021 at 21:11 UTC