proposition: Lemma cardinal_decreases : forall (A:Ensemble U) (f:U -> V) (n:nat), cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n.
proof: Proof. induction 1 as [| A n H'0 H'1 x H'2]; auto with sets. - rewrite (image_empty f); intros. cut (n' = 0). + intro E; rewrite E; trivial with sets. + apply cardinal_unicity with V (Empty_set V); auto with sets. - intro n'. rewrite (Im_add A x f). elim cardinal_Im_intro with A f n; trivial with sets. intros p C H'3. apply Nat.le_trans with (S p). + apply card_Add_gen with V (Im A f) (f x); trivial with sets. + apply -> Nat.succ_le_mono; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts