Library Float.sTactic
Theorem Contradict1 : ∀ a b : Prop, b → (a → ¬ b) → ¬ a.
intuition.
Qed.
Theorem Contradict2 : ∀ a b : Prop, b → ¬ b → a.
intuition.
Qed.
Theorem Contradict3 : ∀ a : Prop, a → ¬ ¬ a.
auto.
Qed.
Ltac Contradict name :=
(apply (fun a : Prop ⇒ Contradict1 a _ name); clear name; intros name) ||
(apply (fun a : Prop ⇒ Contradict2 a _ name); clear name);
try apply Contradict3.
Ltac CaseEq name :=
generalize (refl_equal name); pattern name at -1 in |- *; case name.
Ltac Casec name := case name; clear name.
Ltac Elimc name := elim name; clear name.