From c73c1dbb63b690ccea911ffe39e9776c8da38c04 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Apr 2015 06:20:06 -0700 Subject: [PATCH] feat(library/data/nat/sub): add two extra theorems --- library/data/nat/sub.lean | 7 +++++++ 1 file changed, 7 insertions(+) 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) :=