Definition fincard_standardSubset {n : nat} (P : DecidableSubtype (⟦ n ⟧)) : nat := fincard (subsetFiniteness (isfinitestn n) P). Local Definition bound01 (P : DecidableProposition) : ((choice P 1 0) ≤ 1)%nat. Proof. unfold choice. choose P p q; reflexivity. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.