proposition: Lemma iskfinite_binary_union {X : UU} (A B : hsubtype X) (afinite : iskfinite A) (bfinite : iskfinite B) : iskfinite (A ∪ B).
proof: Proof. use(hinhfun2 _ afinite bfinite). intros afinstruct bfinstruct. use make_kfinstruct. - exact(kfinstruct_cardinality afinstruct + kfinstruct_cardinality bfinstruct). - refine(coprod_carrier_binary_union A B ∘ _). refine(coprodf afinstruct bfinstruct ∘ _). apply weqfromcoprodofstn. - apply issurjcomp. apply issurjcomp. * apply issurjectiveweq, isweqinvmap. * apply issurjective_coprodf; apply issurjective_kfinstruct. * exact(issurjective_coprod_carrier_binary_union A B). Qed.
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.StandardFiniteSets UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.KFiniteTypes