aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool/Bool.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Bool/Bool.v')
-rw-r--r--theories/Bool/Bool.v6
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.