Trivial fact about multiplication of nats

Stream: Is there code for X?

[Stuart Presnell]

This feels like a stupid question, but are there existing lemmas that do this:

example {a b : ℕ} (hab: 0 < a * b) : 0 < a := (left_ne_zero_of_mul hab.ne').bot_lt
example {a b : ℕ} (hab: 0 < a * b) : 0 < b := (right_ne_zero_of_mul hab.ne').bot_lt

[Eric Wieser]

My guess would be pos_of_mul_pos, which leads to docs#pos_of_mul_pos_left and docs#pos_of_mul_pos_right.

[Stuart Presnell]

That's close, but it needs the extra premise that the other multiplicand is positive.

[Yaël Dillies]

There should be a canonically_ordered_semiring variant

[Floris van Doorn]

docs#canonically_ordered_comm_semiring.mul_pos does both

[Stuart Presnell]

Ah fantastic, thanks!

[Stuart Presnell]

Although that ends up giving

(canonically_ordered_comm_semiring.mul_pos.mp hab).1

which is longer than

(left_ne_zero_of_mul hab.ne').bot_lt

:)

[Floris van Doorn]

The order.ring and order.field files need some more care at some point. @Damiano Testa refactored the ordered monoid and group lemmas, but didn't reach the ring/field lemmas yet.

[Stuart Presnell]

Until that gets done would it be ok to submit a PR to data/nat/basic with these two lemmas?

[Eric Wieser]

pos_of_mul_pos_left hab b.zero_le?

[Stuart Presnell]

Ah, of course! The second premise just says that the other argument is non-negative, which of course it is. Thanks!