# Zulip Chat Archive

## Stream: general

### Topic: nat.mul_le_mul

#### Kevin Buzzard (Jun 29 2020 at 10:08):

Is it intentional that `nat.mul_le_mul`

asks twice for proofs that 0 <= (n : nat)? Is this for some general consistency with mul_le_mul lemmas? I thought the whole point of namespaced lemmas like that was precisely so you could change the inputs appropriately.

#### Johan Commelin (Jun 29 2020 at 10:09):

I guess it is not.

#### Johan Commelin (Jun 29 2020 at 10:10):

Probably an artifact from me reproving a bunch of lemmas specifically for `nat`

when ripping algebra out of core.

#### Johan Commelin (Jun 29 2020 at 10:10):

I guess this is in core?

#### Bryan Gin-ge Chen (Jun 29 2020 at 10:10):

Yep: src#nat.mul_le_mul

#### Johan Commelin (Jun 29 2020 at 10:12):

Surrounding lemmas have the same problem.

#### Johan Commelin (Jun 29 2020 at 10:19):

I'm trying to fix this, but lean spits out loads of unrelated errors...

#### Johan Commelin (Jun 29 2020 at 10:20):

Is github down for everyone or just me?

#### Kevin Buzzard (Jun 29 2020 at 10:20):

maybe everyone?

#### Shing Tak Lam (Jun 29 2020 at 10:21):

Everyone

#### Johan Commelin (Jun 29 2020 at 10:21):

Stupid github

#### Kevin Buzzard (Jun 29 2020 at 10:21):

back now but slow

#### Johan Commelin (Jun 29 2020 at 10:23):

https://github.com/leanprover-community/lean/compare/fix-nat-lemmas?expand=1

Last updated: Dec 20 2023 at 11:08 UTC