diff options
Diffstat (limited to 'flocq/Core/Zaux.v')
| -rw-r--r-- | flocq/Core/Zaux.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/flocq/Core/Zaux.v b/flocq/Core/Zaux.v index b14c4e93..57e351dd 100644 --- a/flocq/Core/Zaux.v +++ b/flocq/Core/Zaux.v @@ -773,6 +773,12 @@ End Zcompare. Section cond_Zopp. +Theorem cond_Zopp_0 : + forall sx, cond_Zopp sx 0 = 0%Z. +Proof. +now intros [|]. +Qed. + Theorem cond_Zopp_negb : forall x y, cond_Zopp (negb x) y = Z.opp (cond_Zopp x y). Proof. |