proposition: Lemma Zrnd_odd_plus': forall x y, (exists n:Z, exists e:Z, (x = IZR n*bpow beta e)%R /\ (1 <= e)%Z) -> (IZR (Zrnd_odd (x+y)) = x+IZR (Zrnd_odd y))%R.
proof: Proof. intros x y (n,(e,(H1,H2))). apply Zrnd_odd_plus. rewrite H1. rewrite <- IZR_Zpower. 2: auto with zarith. now rewrite <- mult_IZR, Zfloor_IZR. rewrite H1, <- IZR_Zpower. 2: auto with zarith. rewrite <- mult_IZR, Zfloor_IZR. rewrite Z.even_mul. rewrite Z.even_pow. 2: auto with zarith. rewrite Even_beta. apply Bool.orb_true_iff; now right. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations