Definition tallyStandardSubset {n : nat} (P : DecidableSubtype (⟦ n ⟧)) : ⟦ S n ⟧. Proof. exists (stnsum (λ x, choice (P x) 1 0)). apply natlehtolthsn. apply (istransnatleh (m := stnsum(λ _ : stn n, 1))). { apply stnsum_le; intro i. apply bound01. } assert (p : ∏ r s : nat, r = s -> (r ≤ s)%nat). { intros ? ? e. destruct e. apply isreflnatleh. } apply p. exact(stnsum_1 n). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.