proposition: Lemma FiniteT_nat_cardinal_option: forall (X:Type) (H:FiniteT X), FiniteT_nat_cardinal (option X) (add_finite X H) = S (FiniteT_nat_cardinal X H).
proof: Proof. intros. apply FiniteT_nat_cardinal_cond. rewrite option_Full_set_Im. constructor. - apply injection_preserves_cardinal. + apply FiniteT_nat_cardinal_def. + red; intros x1 x2 Heq; injection Heq; trivial. - red; intro. inversion H0. discriminate H2. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)