proposition: Lemma equiv_RNDs_aux: forall z, Z.even z = true -> Even z.
proof: Proof. intros z; unfold Z.even, Even. case z. intros; exists 0%Z; auto with zarith. intros p0; case p0. intros p1 H; contradict H; auto. intros p1 _. exists (Zpos p1); auto with zarith. intros H; contradict H; auto. intros p0; case p0. intros p1 H; contradict H; auto. intros p1 _. exists (Zneg p1); auto with zarith. intros H; contradict H; auto. Qed.
imports: Coq(Lia) Pff Core