proposition: Lemma C_format: format (bpow s +1).
proof: Proof. Proof with auto with typeclass_instances. apply generic_format_FLT. exists (Defs.Float beta (Zpower beta s+1)%Z 0%Z); simpl. unfold F2R; simpl. rewrite plus_IZR, IZR_Zpower; try lia. simpl; ring. rewrite Z.abs_eq. apply Z.le_lt_trans with (beta^s+beta^0)%Z. simpl; lia. apply Z.le_lt_trans with (beta^s+beta^s)%Z. apply Zplus_le_compat_l. apply Zpower_le; lia. apply Z.le_lt_trans with (2*beta^s)%Z. lia. apply Z.le_lt_trans with (beta^1*beta^s)%Z. apply Zmult_le_compat_r. rewrite Z.pow_1_r. apply Zle_bool_imp_le; apply beta. apply Zpower_ge_0. rewrite <- Zpower_plus; try lia. apply Zpower_lt; lia. apply Z.le_trans with (beta^s)%Z; try lia. apply Zpower_ge_0. assumption. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat