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. assert (Full_set = Add (Im Full_set (@Some X)) None). apply Extensionality_Ensembles; split. red; intros. destruct x. left; exists x; constructor. right; constructor. red; intros; constructor. rewrite H0. constructor. apply injection_preserves_cardinal. apply FiniteT_nat_cardinal_def. red; intros x1 x2 Heq; injection Heq; trivial. red; intro. inversion H1. discriminate H3. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description FunctionalExtensionality