proposition: Lemma Zrnd_odd_Zodd: forall x, x <> (IZR (Zfloor x)) -> (Z.even (Zrnd_odd x)) = false.
proof: Proof. intros x Hx; unfold Zrnd_odd. destruct (Req_EM_T x (IZR (Zfloor x))) as [H|H]. now contradict H. case_eq (Z.even (Zfloor x)). intros H'. rewrite Zceil_floor_neq. rewrite Z.even_add, H'. reflexivity. now apply sym_not_eq. trivial. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations