proposition: Theorem InRzDec : forall (a : rZ) (L : list rZ), {InRz a L} + {~ InRz a L}.
proof: Proof. intros a L; elim L; auto with stalmarck. right; red in |- *; intros H'; inversion H'. intros a0 l H'; case H'. intros H'0; left; auto with stalmarck. red in |- *; apply InEqSkip; auto with stalmarck. intros H'0; case (rNatDec (valRz a) (valRz a0)); intros H'1. left; auto with stalmarck. red in |- *; apply InEqHead; auto with stalmarck. right; red in |- *; intros H'2; inversion_clear H'2. case H'1; auto with stalmarck. case H'0; auto with stalmarck. Qed.