proposition: Theorem inMapComp : forall (a : rZ) (L : list rZ), In (rZComp a) (map rZComp L) -> In a L.
proof: Proof. intros a L; elim L; simpl in |- *; auto with stalmarck. intros a0 l H' H'0; Elimc H'0; auto with stalmarck. left; apply rZCompEq; auto with stalmarck. Qed.