proposition: Lemma LeExp: (powerRZ radix (Fexp ph)+powerRZ radix (Fexp uh) <= 2*powerRZ radix (Fexp z+1))%R.
proof: Proof. apply Rle_trans with (powerRZ radix (Fexp z + 1)+ powerRZ radix (Fexp z + 1))%R;[idtac|right; ring]. apply Rplus_le_compat; apply Rle_powerRZ; try apply IZR_le; auto with real zarith. generalize LeExp1; generalize LeExp2; generalize LeExp3; intros. case (Zle_lt_or_eq _ _ H0); intros; auto with zarith. generalize LeExp1; generalize LeExp2; generalize LeExp3; intros; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz