diff options
Diffstat (limited to 'theories/Bool/Bool.v')
| -rw-r--r-- | theories/Bool/Bool.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 0d674ebf9..652ac955e 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -308,6 +308,12 @@ Hint Resolve orb_comm orb_assoc: bool v62. (** * Properties of [andb] *) (*******************************) +Lemma andb_true_iff : + forall b1 b2:bool, b1 && b2 = true <-> b1 = true /\ b2 = true. +Proof. + destruct b1; destruct b2; intuition. +Qed. + Lemma andb_true_eq : forall a b:bool, true = a && b -> true = a /\ true = b. Proof. |