proposition: Theorem InEqInv : forall (a : rZ) (L : list rZ), InRz a L -> In a L \/ In (rZComp a) L.
proof: Proof. intros a L H'; Elimc H'; clear a L; auto with stalmarck. intros a b L; case a; case b; unfold eqRz in |- *; simpl in |- *; intros a' b' Eqt; rewrite Eqt; auto with stalmarck. intros a b L H' H'0; elim H'0; auto with datatypes stalmarck. Qed.