proposition: Lemma injection_preserves_cardinal: forall (X Y:Type) (f:X->Y) (n:nat) (S:Ensemble X), cardinal S n -> injective f -> cardinal (Im S f) n.
proof: Proof. intros. induction H. - rewrite image_empty. constructor. - rewrite Im_add. constructor; trivial. red; intro H3; inversion H3. subst. apply H0 in H4. subst. contradiction. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)