# Zulip Chat Archive

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

s

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