proposition: Lemma diff_comp : forall A A' B B' : part_set E, Equal A A' -> Equal B B' -> Equal (diff A B) (diff A' B').
proof: Proof. intros A A' B B'; try assumption. unfold diff in |- *; simpl in |- *. unfold eq_part in |- *; simpl in |- *. intros H' H'0 x; split; [ intros H'1; split; [ try assumption | idtac ] | idtac ]. elim (H' x); intros H'3 H'4; lapply H'3; [ intros H'5; try exact H'5; clear H'3 | clear H'3 ]. elim H'1; intros H'2 H'3; try exact H'2; clear H'1. red in |- *. intros H'2; try assumption. absurd (in_part x B); auto with algebra. elim H'1; intros H'3 H'4; try exact H'4; clear H'1. elim (H'0 x); intros H'4 H'5; lapply H'5; [ intros H'6; try exact H'6; clear H'5 | clear H'5 ]. auto with algebra. intros H'1; split; [ try assumption | idtac ]. elim (H' x); intros H'3 H'4; lapply H'4; [ intros H'5; try exact H'5; clear H'4 | clear H'4 ]. elim H'1; intros H'2 H'4; try exact H'2; clear H'1. red in |- *. intros H'2; try assumption. absurd (in_part x B'); auto with algebra. elim H'1; intros H'3 H'4; try exact H'4; clear H'1. elim (H'0 x); intros H'4 H'5; lapply H'4; [ intros H'6; try exact H'6; clear H'4 | clear H'4 ]. try exact H'2. Qed.
imports: Parts