diff options
Diffstat (limited to 'theories/Bool')
| -rw-r--r-- | theories/Bool/Bool.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index f4649be04..437ce5726 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -555,6 +555,21 @@ Proof. destr_bool. Qed. +Lemma negb_xorb_l : forall b b', negb (xorb b b') = xorb (negb b) b'. +Proof. + destruct b,b'; trivial. +Qed. + +Lemma negb_xorb_r : forall b b', negb (xorb b b') = xorb b (negb b'). +Proof. + destruct b,b'; trivial. +Qed. + +Lemma xorb_negb_negb : forall b b', xorb (negb b) (negb b') = xorb b b'. +Proof. + destruct b,b'; trivial. +Qed. + (** Lemmas about the [b = true] embedding of [bool] to [Prop] *) Lemma eq_iff_eq_true : forall b1 b2, b1 = b2 <-> (b1 = true <-> b2 = true). |