Library Float.sTactic



Theorem Contradict1 : a b : Prop, b → (a¬ b) → ¬ a.
intuition.
Qed.

Theorem Contradict2 : a b : Prop, b¬ ba.
intuition.
Qed.

Theorem Contradict3 : a : Prop, a¬ ¬ a.
auto.
Qed.

Ltac Contradict name :=
  (apply (fun a : PropContradict1 a _ name); clear name; intros name) ||
    (apply (fun a : PropContradict2 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.