diff options
Diffstat (limited to 'lib/Coqlib.v')
| -rw-r--r-- | lib/Coqlib.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 58c9572..35d5385 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -177,6 +177,9 @@ Proof (Pos.lt_irrefl). Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. +Ltac xomega := unfold Plt, Ple in *; zify; omega. +Ltac xomegaContradiction := exfalso; xomega. + (** Peano recursion over positive numbers. *) Section POSITIVE_ITERATION. |