diff options
Diffstat (limited to 'theories/Bool/Bool.v')
| -rw-r--r-- | theories/Bool/Bool.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index b13369368..f4649be04 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -257,6 +257,11 @@ Proof. intros. apply orb_false_iff; trivial. Qed. +Lemma orb_diag : forall b, b || b = b. +Proof. + destr_bool. +Qed. + (** [true] is a zero for [orb] *) Lemma orb_true_r : forall b:bool, b || true = true. @@ -362,6 +367,11 @@ Qed. Notation andb_b_false := andb_false_r (only parsing). Notation andb_false_b := andb_false_l (only parsing). +Lemma andb_diag : forall b, b && b = b. +Proof. + destr_bool. +Qed. + (** [true] is neutral for [andb] *) Lemma andb_true_r : forall b:bool, b && true = b. |