Zulip Chat Archive

Stream: Is there code for X?

Topic: sq_sub_sq for nat


view this post on Zulip Ruben Van de Velde (Sep 11 2020 at 21:39):

example (a b : ) (h : b  a) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := sorry

view this post on Zulip Johan Commelin (Sep 12 2020 at 03:30):

Hmm, maybe we only have this for comm_rings

view this post on Zulip Johan Commelin (Sep 12 2020 at 03:31):

You could either prove it by hand, or use the zify tactic to deduce it from the fact for int.

view this post on Zulip Alex J. Best (Sep 12 2020 at 03:37):

h isn't necessary as an assumption I don't think, if a < b then both sides are 0.

view this post on Zulip Bryan Gin-ge Chen (Sep 12 2020 at 04:03):

Oh, we have docs#nat.mul_self_sub_mul_self_eq, but not nat.pow_two_sub_pow_two, even though we have both docs#mul_self_sub_mul_self_eq (which is redundant with docs#mul_self_sub_mul_self) and docs#pow_two_sub_pow_two.

view this post on Zulip Bryan Gin-ge Chen (Sep 12 2020 at 04:08):

#4119 removes mul_self_sub_mul_self_eq. It's getting late so I'll leave it to someone else to add nat.pow_two_sub_pow_two.

view this post on Zulip Bryan Gin-ge Chen (Sep 12 2020 at 22:49):

Update: I was going to add nat.pow_two_sub_pow_two but it's turned into a cleanup of data.nat.basic instead, which I'll try to PR sometime tomorrow.

view this post on Zulip Bryan Gin-ge Chen (Sep 13 2020 at 21:29):

PR is here: #4135


Last updated: May 17 2021 at 16:26 UTC