add inverses of bool_decide_{true,false}

theories/decidable.v

@@ -120,6 +120,15 @@ Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
   (P ↔ Q) → bool_decide P = bool_decide 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.
+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. }
+  destruct (bool_decide P). discriminate. contradiction.
+Qed.
+
 (** * Decidable Sigma types *)
 (** Leibniz equality on Sigma types requires the equipped proofs to be
 equal as Coq does not support proof irrelevance. For decidable we