diff --git a/library/data/bool.lean b/library/data/bool.lean
index 7407d1558..09c8aa08a 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -68,6 +68,12 @@ namespace bool
       or.inr Hb)
     (assume H, or.inl rfl)
 
+  theorem bor_inl {a b : bool} (H : a = tt) : a || b = tt :=
+  by rewrite H
+
+  theorem bor_inr {a b : bool} (H : b = tt) : a || b = tt :=
+  bool.rec_on a (by rewrite H) (by rewrite H)
+
   theorem ff_band (a : bool) : ff && a = ff :=
   rfl
 
@@ -104,6 +110,9 @@ namespace bool
         ff_ne_tt)
     (assume H1 : a = tt, H1)
 
+  theorem band_intro {a b : bool} (H₁ : a = tt) (H₂ : b = tt) : a && b = tt :=
+  by rewrite [H₁, H₂]
+
   theorem band_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
   band_elim_left (!band.comm ⬝ H)