2 files changed, 17 insertions, 14 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 8f739e0dac..0d674ebf93 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -308,26 +308,12 @@ Hint Resolve orb_comm orb_assoc: bool v62.
 (** * Properties of [andb]     *)
 (*******************************)
 
-Lemma andb_prop : forall a b:bool, a && b = true -> a = true /\ b = true.
-Proof.
-  destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
-    auto with bool.
-Qed.
-Hint Resolve andb_prop: bool v62.
-
 Lemma andb_true_eq :
   forall a b:bool, true = a && b -> true = a /\ true = b.
 Proof.
   destruct a; destruct b; auto.
 Defined.
 
-Lemma andb_true_intro :
-  forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true.
-Proof.
-  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
-Qed.
-Hint Resolve andb_true_intro: bool v62.
-
 Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false.
 Proof.
   destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 912192b268..3525908ab6 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -51,6 +51,23 @@ Definition negb (b:bool) := if b then false else true.
 Infix "||" := orb (at level 50, left associativity) : bool_scope.
 Infix "&&" := andb (at level 40, left associativity) : bool_scope.
 
+(*******************************)
+(** * Properties of [andb]     *)
+(*******************************)
+
+Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
+Proof.
+  destruct a; destruct b; intros; split; try (reflexivity || discriminate).
+Qed.
+Hint Resolve andb_prop: bool v62.
+
+Lemma andb_true_intro :
+  forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
+Proof.
+  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+Qed.
+Hint Resolve andb_true_intro: bool v62.
+
 (** Interpretation of booleans as propositions *)
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.