blob: 2d1ab6c58e90ec8c3cb4e96964bb6fa4afae0659 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Require Import Coq.Arith.Arith Coq.Arith.Max.
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_r by
(exact H)
| [ H : ~ (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite max_l by
(exact (le_Sn_le _ _ (not_le _ _ H)))
end
end.
Lemma pull_app_if_sumbool {A B X Y} (b : sumbool X Y) (f g : A -> B) (x : A)
: (if b then f x else g x) = (if b then f else g) x.
Proof.
destruct b; reflexivity.
Qed.
|
