proposition: Lemma cardinal_included : forall (E : Setoid) (A : part_set E) (n : nat), cardinal A n -> forall B : part_set E, included B A -> exists m : nat, cardinal B m /\ m <= n.
proof: Proof. intros E A n H'; try assumption. apply cardinal_ind2 with (P := fun (n : nat) (A : part_set E) (c : cardinal A n) => forall B : part_set E, included B A -> ex (fun m : nat => cardinal B m /\ m <= n)). intros A0 H'0 B H'1; exists 0; split; [ try assumption | idtac ]; auto with *. apply cardinal_empty. inversion H'0. cut (included B (empty E)); auto with *. apply included_comp with B A0; auto with *. intros n0 H'0 A0 B x H'1 H'2 H'3 B0 H'4; try assumption. case (classic (Equal B0 A0)); intros. exists (S n0); split; [ idtac | try assumption ]. apply cardinal_comp with A0 (S n0); auto with *. auto with *. case (not_included_exist H'4 H). intros x0 H'5; try assumption. elim H'5; intros H'6 H'7; try exact H'6; clear H'5. lapply (H'0 (minus_part A0 x0)); [ intros H'8; elim (H'8 B0); [ intros m E0; elim E0; intros H'11 H'12; try exact H'11; clear E0 | idtac ] | idtac ]; auto with *. exists m; split; [ try assumption | idtac ]. apply le_trans with n0; auto with *. unfold minus_part in |- *; simpl in |- *. red in |- *. intros x1 H'5; try assumption. simpl in |- *. split; [ try assumption | idtac ]. apply H'4; auto with *. red in |- *. intros H'9; try assumption. apply H'7. apply in_part_comp_l with x1; auto with *. apply cardinal_S with A0 x0; auto with *. apply Sym. apply minus_add; auto with *. auto with *. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec