proposition: Lemma bool_decide_rel_true `(R : relation A) {dec : ∀ x y, Decision (R x y)} : ∀ x y, bool_decide_rel R x y ≡ true ↔ R x y.
proof: Proof. unfold bool_decide_rel. split; intro; destruct dec; firstorder with bool. Qed.
imports: MathClasses.interfaces.canonical_names MathClasses.misc.util