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

chore(hott/types/nat/order): remove occurrence of "migrate" command

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-08 15:37:13 -08:00
parent b145a7332a
commit 6404c3c014
1 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
hott/types/nat/order.hlean
View file

@ -135,9 +135,17 @@ section
mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left, mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left,
mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right ⦄ mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right ⦄
migrate from algebra with nat variables {a b c d : nat}
replacing has_le.ge → ge, has_lt.gt → gt theorem ne_of_lt (lt_ab : a < b) : a ≠ b := algebra.ne_of_lt lt_ab
hiding pos_of_mul_pos_left, pos_of_mul_pos_right, lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right theorem ne_of_gt (gt_ab : a > b) : a ≠ b := algebra.ne_of_gt gt_ab
theorem lt_of_not_le (H : ¬ a ≥ b) : a < b := algebra.lt_of_not_le H
theorem le_or_gt (a b : nat) : sum (a ≤ b) (a > b) := algebra.le_or_gt a b
theorem le_of_mul_le_mul_left (H : c * a ≤ c * b) (Hc : c > 0) : a ≤ b := algebra.le_of_mul_le_mul_left H Hc
theorem not_lt_of_le (H : a ≤ b) : ¬ b < a := algebra.not_lt_of_le H
theorem not_le_of_lt (H : a < b) : ¬ b ≤ a := algebra.not_le_of_lt H
theorem add_le_add (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d := algebra.add_le_add Hab Hcd
theorem lt_of_add_lt_add_right (H : a + b < c + b) : a < c := algebra.lt_of_add_lt_add_right H
theorem lt_of_add_lt_add_left (H : a + b < a + c) : b < c := algebra.lt_of_add_lt_add_left H
end end
section port_algebra section port_algebra