add inverses of bool_decide_{true,false}

theories/decidable.v

@@ -121,13 +121,9 @@ Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
 Proof. repeat case_bool_decide; tauto. Qed.
 
 Lemma bool_decide_true_2 P `{!Decision P}: bool_decide P = true → P.
-Proof. intros Heq. eapply bool_decide_unpack. rewrite Heq. exact I. Qed.
+Proof. case_bool_decide; auto || discriminate.  Qed.
 Lemma bool_decide_false_2 P `{!Decision P}: bool_decide P = false → ¬P.
-Proof.
-  intros Heq HP. assert (HP': bool_decide P).
-  { apply bool_decide_spec. assumption. }
-  case_bool_decide; auto || discriminate.
-Qed.
+Proof. case_bool_decide; auto || discriminate. Qed.
 
 (** * Decidable Sigma types *)
 (** Leibniz equality on Sigma types requires the equipped proofs to be