Extensions to finset (sum) and auxiliary lemmas.

[helm.git] / matita / matita / lib / basics / bool.ma

diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma
index fb0106f12501b1d1b951f64dd912d669a1618203..587ab9ed6fde1a22ce752675be2313aaa60df731 100644 (file)
--- a/matita/matita/lib/basics/bool.ma
+++ b/matita/matita/lib/basics/bool.ma
@@ -54,6 +54,10 @@ theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
 match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
 #b1 #b2 #P (elim b1) normalize // qed.
 
+theorem true_to_andb_true: ∀b1,b2. b1 = true → b2 = true → (b1 ∧ b2) = true.
+#b1 cases b1 normalize //
+qed.
+
 theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
 #b1 (cases b1) normalize // qed.