michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/nat/sub): add two extra theorems

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-14 06:20:06 -07:00
parent 11c9bb4626
commit c73c1dbb63
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/data/nat/sub.lean
View file

@ -148,6 +148,13 @@ calc
... = n * m - k * n : {!mul.comm} ... = n * m - k * n : {!mul.comm}
... = n * m - n * k : {!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 -/ /- interaction with inequalities -/
theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n = succ (m - n) := theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n = succ (m - n) :=