sq_sub_sq for nat

Stream: Is there code for X?

[Ruben Van de Velde]

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

[Johan Commelin]

Hmm, maybe we only have this for comm_rings

[Johan Commelin]

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

[Alex J. Best]

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

[Bryan Gin-ge Chen]

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]

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

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]

PR is here: #4135