proposition: Lemma Zrnd_odd_plus: forall x y, (x = IZR (Zfloor x)) -> Z.even (Zfloor x) = true -> (IZR (Zrnd_odd (x+y)) = x+IZR (Zrnd_odd y))%R.
proof: Proof. intros x y Hx H. unfold Zrnd_odd; rewrite Hx, Zfloor_plus. case (Req_EM_T y (IZR (Zfloor y))); intros Hy. rewrite Hy; repeat rewrite <- plus_IZR. repeat rewrite Zfloor_IZR. case (Req_EM_T _ _); intros K; easy. case (Req_EM_T _ _); intros K. contradict Hy. apply Rplus_eq_reg_l with (IZR (Zfloor x)). now rewrite K, plus_IZR. rewrite Z.even_add, H; simpl. case (Z.even (Zfloor y)). now rewrite Zceil_plus, plus_IZR. now rewrite plus_IZR. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations