proposition: Lemma Decides_false {A} : forall (P : Ensemble A) (P_dec : DecideableEnsemble P) a, dec a = false <-> ~ (P a).
proof: Proof. split; unfold not; intros. + apply dec_decides_P in H0; congruence. + case_eq (dec a); intros; eauto. apply dec_decides_P in H0; intuition. Qed.
imports: Fiat.Common Coq.Arith.Arith Coq.Bool.Bool Coq.Sets.Ensembles