Ici (0 : Nat) = univ

Stream: Is there code for X?

[Ruben Van de Velde]

@Yaël Dillies this sounds likes something you'd have written :)

(It's just a docs#bot_eq_zero away from docs#Ici_bot , but that's kinda unintuitive in my opinion)

[Ruben Van de Velde]

Actually, the code I'm looking at is for (0 : ℝ≥0∞), but same question

[Yaël Dillies]

Nope. We don't have that. Correct generality is CanonicallyOrderedAddCommMonoid.

[Ruben Van de Velde]

Would it be worth adding / where should it go?

[Yaël Dillies]

I'm honestly not so in favour of duplicating all bot lemmas to zero.

[Yaël Dillies]

I would only be favour when there's a simp confluence issue.

[Eric Wieser]

I think there's a simp feature request hiding here; simp already knows how to apply add_comm in moderation without causing loops. Perhaps it could learn to apply bot_eq_zero and zero_eq_bot (or whatever the lemmas are called) simultaneously without loop.