proposition: Lemma not_included_exist : forall (E : Setoid) (A B : part_set E), included B A -> ~ Equal B A -> exists x : E, in_part x A /\ ~ in_part x B.
proof: Proof. intros E A B; simpl in |- *. unfold eq_part in |- *; simpl in |- *. intros H' H'0; try assumption. cut (ex (fun x : E => ~ ((in_part x B -> in_part x A) /\ (in_part x A -> in_part x B)))). intros H'1; try assumption. elim H'1; intros x E0; try exact E0; clear H'1. exists x; split; [ try assumption | idtac ]. red in E0. apply NNPP. red in |- *; intros H'1; try exact H'1. lapply E0; [ intros H'2; apply H'2; clear E0 | clear E0 ]. split; [ idtac | intros H'2; try assumption ]. intros H'2; try assumption. apply H'; auto with *. absurd (in_part x A); auto with *. red in |- *. red in E0. intros H'1; try assumption. lapply E0; [ intros H'2; apply H'2; clear E0 | clear E0 ]. split; [ try assumption | idtac ]. intros H'2; try assumption. apply H'; auto with *. auto with *. apply not_all_ex_not with (P := fun x : E => (in_part x B -> in_part x A) /\ (in_part x A -> in_part x B)); auto with *. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec