proposition: Lemma cardinal_image_lesser : forall (E F : Setoid) (f : MAP E F) (A : part_set E) (n : nat), cardinal A n -> exists m : nat, cardinal (image f A) m /\ m <= n.
proof: Proof. intros E F f A n H'; try assumption. apply cardinal_ind2 with (P := fun (n : nat) (A : part_set E) (c : cardinal A n) => ex (fun m : nat => cardinal (image f A) m /\ m <= n)). intros A0 H'0; try assumption. exists 0; split; [ idtac | auto with * ]. apply cardinal_empty; auto with *. intros n0 H'0 A0 B x H'1 H'2 H'3; try assumption. case (classic (in_part (f x) (image f B))). intros H'4; try assumption. elim (H'0 B); [ intros m E0; elim E0; intros H'7 H'8; try exact H'7; clear E0 | idtac ]. exists m; split; [ idtac | try assumption ]. apply cardinal_comp with (image f B) m; auto with *. apply Sym. apply Trans with (image f (add_part B x)); auto with *. unfold add_part in |- *. apply Trans with (union (image f B) (image f (single x))); auto with *. apply Trans with (union (image f B) (single (Ap f x))); auto with *. auto with *. apply cardinal_S with A0 x; auto with *. intros H'4; try assumption. elim (H'0 B); [ intros m E0; elim E0; intros H'7 H'8; try exact H'7; clear E0 | idtac ]. exists (S m); split; [ try assumption | idtac ]. apply cardinal_add with (image f B) (Ap f x); auto with *. unfold add_part in |- *. unfold add_part in H'2. apply Trans with (image f (union B (single x))); auto with *. apply Trans with (union (image f B) (image f (single x))); auto with *. auto with *. apply cardinal_S with A0 x; auto with *. auto with *. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec