proposition: Lemma finite_prod: forall (X Y:Type), FiniteT X -> FiniteT Y -> FiniteT (X*Y).
proof: Proof. intros. induction H0. - apply bij_finite with _ (False_rect _). + constructor. + exists (@snd X False). * destruct x. * destruct y. destruct f. - pose (g := fun (x:X*T + X) => match x with | inl (pair x0 t) => pair x0 (Some t) | inr x0 => pair x0 None end). pose (ginv := fun (x:X * option T) => match x with | (x0, Some t) => inl _ (x0, t) | (x0, None) => inr _ x0 end). apply bij_finite with _ g. + apply finite_sum; assumption. + exists ginv. * destruct x as [[x0 t]|x0]; trivial. * destruct y as [x0 [t|]]; trivial. - pose (g := fun (y:X*X0) => match y with | pair x x0 => pair x (f x0) end). destruct H1. pose (ginv := fun (y:X*Y) => let (x,y0) := y in (x, g0 y0)). apply bij_finite with _ g. { assumption. } exists ginv. + destruct x as [x x0]; unfold ginv, g; try rewrite H1; trivial. + destruct y as [x y]; unfold ginv, g; try rewrite H2; trivial. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)