proposition: Lemma maxval_lt : maxval < Rpow2 emax.
proof: Proof. unfold maxval. replace emax with (prec + (emax - prec))%Z at 2 by now rewrite Z.add_comm, Z.sub_add. rewrite bpow_plus. apply Rmult_lt_compat_r; [apply bpow_gt_0 |]. rewrite minus_IZR. rewrite IZR_Zpower by easy. apply (Rplus_lt_reg_r 1). unfold Rminus. rewrite Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_r. apply Rlt_plus_1. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)