proposition: Lemma image_in_image : forall (A : part_set E) (x : E), in_part x A -> in_part (f x) (image A).
proof: Proof. simpl in |- *; auto with algebra. intros A x H'; try assumption. exists x; split; [ try assumption | idtac ]; auto with algebra. Qed.
imports: Classical_Prop Parts