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

fix(library/algebra/order): duplicate argument

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-03 17:04:26 -08:00
parent e2bef88a33
commit 6ad469e717
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/algebra/order.lean
View file

@ -306,7 +306,7 @@ section
(assume H, or.elim H (assume H', H2 H') (assume H', H3 H'))
definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion] [reducible]
[s : linear_strong_order_pair A] : linear_order_pair A :=
: linear_order_pair A :=
⦃ linear_order_pair, s ⦄
theorem le_of_not_lt {a b : A} (H : ¬ a < b) : b ≤ a :=