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

feat(library/data/nat/order): add calc_trans commands for lt and le

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-17 23:44:27 -08:00
parent 5dc42762de
commit e2ceb86884
1 changed files with 21 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
library/data/nat/order.lean
View file

@ -334,6 +334,27 @@ le_trans (succ_le H1) H2
theorem lt_trans {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k := theorem lt_trans {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k :=
lt_le_trans H1 (lt_imp_le H2) lt_le_trans H1 (lt_imp_le H2)
theorem eq_le_trans {n m k : ℕ} (H1 : n = m) (H2 : m ≤ k) : n ≤ k :=
H1⁻¹ ▸ H2
theorem eq_lt_trans {n m k : ℕ} (H1 : n = m) (H2 : m < k) : n < k :=
H1⁻¹ ▸ H2
theorem le_eq_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m = k) : n ≤ k :=
H2 ▸ H1
theorem lt_eq_trans {n m k : ℕ} (H1 : n < m) (H2 : m = k) : n < k :=
H2 ▸ H1
calc_trans le_trans
calc_trans lt_trans
calc_trans lt_le_trans
calc_trans le_lt_trans
calc_trans eq_le_trans
calc_trans eq_lt_trans
calc_trans le_eq_trans
calc_trans lt_eq_trans
theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m := theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m :=
not_intro (assume H2 : m < n, absurd (le_lt_trans H H2) !lt_irrefl) not_intro (assume H2 : m < n, absurd (le_lt_trans H H2) !lt_irrefl)