proposition: Lemma cardinal_sup3 : forall (A B C : part_set E) (x y : E), Equal A (add_part B x) -> Equal A (add_part C y) -> ~ in_part x B -> ~ in_part y C -> ~ Equal x y -> exists D : part_set E, Equal B (add_part D y) /\ Equal C (add_part D x) /\ ~ in_part x D /\ ~ in_part y D.
proof: Proof. intros. exists (minus_part B y). split. apply Sym. apply minus_add. cut (in_part y (add_part B x)). intros. apply add_part_in_el_diff with x; auto with algebra. apply in_part_comp_r with A; auto with algebra. apply in_part_comp_r with (add_part C y); auto with algebra. split. apply add_part_simpl with y; auto with algebra. unfold not in |- *; intro. absurd (Equal y x); auto with algebra. apply add_part_in_el_not_in with (minus_part B y); auto with algebra. apply Trans with (add_part (add_part (minus_part B y) y) x); auto with algebra. apply Trans with (add_part B x); auto with algebra. apply Trans with A; auto with algebra. apply add_part_comp; auto with algebra. apply Sym. apply minus_add; auto with algebra. apply add_part_in_el_diff with x; auto with algebra. apply in_part_comp_r with (add_part C y); auto with algebra. apply Trans with A; auto with algebra. split. apply minus_trans_not_in; auto with algebra. auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop