blob: 35f207ffcc276a999bf6cf81a8b3b7ab9662f865 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Require Import Arith.
Ltac case_max :=
match goal with [ |- context[max ?x ?y] ] =>
destruct (le_dec x y);
match goal with
| [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_r by
(exact H)
| [ H : ~ (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_l by
(exact (le_Sn_le _ _ (not_le _ _ H)))
end
end.
|
