Definition isfinite_isdeceq (X : UU) : isfinite X -> isdeceq X. Proof. intros isfin. use(factor_through_squash (isapropisdeceq X) _ isfin). intro fstruct. use(isdeceqweqf _ (isdeceqstn (finstruct_cardinality fstruct))). apply fstruct. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.