diff options
Diffstat (limited to 'lib/Integers.v')
-rw-r--r-- | lib/Integers.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 369584c3..066e6b04 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -668,6 +668,11 @@ Proof. intros. generalize (eq_spec x y); case (eq x y); intros; congruence. Qed. +Theorem same_if_eq: forall x y, eq x y = true -> x = y. +Proof. + intros. generalize (eq_spec x y); rewrite H; auto. +Qed. + Theorem eq_signed: forall x y, eq x y = if zeq (signed x) (signed y) then true else false. Proof. |