diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 459f422cce..68534d10d1 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -148,6 +148,13 @@ calc
           ... = n * m - k * n : {!mul.comm}
           ... = n * m - n * k : {!mul.comm}
 
+theorem mul_self_sub_mul_self_eq (a b : nat) : a * a - b * b = (a + b) * (a - b) :=
+by rewrite [mul_sub_left_distrib, *mul.right_distrib, mul.comm b a, add.comm (a*a) (a*b), add_sub_add_left]
+
+theorem succ_mul_succ_eq (a : nat) : succ a * succ a = a*a + a + a + 1 :=
+calc succ a * succ a = (a+1)*(a+1)     : by rewrite [add_one]
+                ...  = a*a + a + a + 1 : by rewrite [mul.right_distrib, mul.left_distrib, one_mul, mul_one]
+
 /- interaction with inequalities -/
 
 theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n  = succ (m - n) :=