## Stream: Is there code for X?

### Topic: sq_sub_sq for nat

#### 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


#### Johan Commelin (Sep 12 2020 at 03:30):

Hmm, maybe we only have this for comm_rings

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

#### Bryan Gin-ge Chen (Sep 13 2020 at 21:29):

PR is here: #4135

Last updated: May 17 2021 at 16:26 UTC