blob: 31588815bc85d27d447d2c0d109bae57f8f24bf0 (
plain)
1
2
3
4
5
6
7
8
|
Require Import Coq.ZArith.ZArith.
Module Z.
Ltac compare_to_sgn :=
repeat match goal with
| [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H
| _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff
end.
End Z.
|
