PR #16525: chore(algebra/order/monoid_lemmas_zero_lt): re...

Stream: triage

[Random Issue Bot]

Today I chose PR 16525 for discussion!

chore(algebra/order/monoid_lemmas_zero_lt): remove useless lemmas, use namespace without_zero_le_one
Created by @None (@negiizhao) on 2022-09-15
Labels: awaiting-review, t-algebra, t-order

Is this PR still relevant? Any recent updates? Anyone making progress?