proposition: Lemma powerRZSumRle: forall (e1 e2:Z), (e2<= e1)%Z -> (powerRZ radix e1 + powerRZ radix e2 <= powerRZ radix (e1+1))%R.
proof: Proof. clear -radixMoreThanOne; intros. apply Rle_trans with (powerRZ radix e1 + powerRZ radix e1)%R; [apply Rplus_le_compat_l; apply Rle_powerRZ; auto with real zarith|idtac]. apply IZR_le; lia. apply Rle_trans with (powerRZ radix e1*2)%R;[right; ring|rewrite powerRZ_add]. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. simpl; ring_simplify (radix*1)%R; apply IZR_le; auto with real zarith. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz