proposition: Lemma bool_decide_false `{dec : !Decision P} : bool_decide P ≡ false ↔ ¬P.
proof: Proof. unfold bool_decide. split; intro; destruct dec; firstorder with bool. Qed.
imports: MathClasses.interfaces.canonical_names MathClasses.misc.util