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
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
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):
mul_self_sub_mul_self_eq. It's getting late so I'll leave it to someone else to add
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