proposition: Lemma Fulp_ulp_aux: forall f, Fcanonic beta b f -> Fulp b beta (Z.abs_nat p) f = ulp beta (FLT_exp (-dExp b) p) (FtoR beta f).
proof: Proof. intros f H. case (Req_dec (FtoR beta f) 0); intros Zf. rewrite Zf, ulp_FLT_small. 2: unfold Prec_gt_0; lia. 2: rewrite Rabs_R0; apply bpow_gt_0. rewrite Fulp_zero. apply sym_eq, bpow_powerRZ. apply is_Fzero_rep2 with beta; try assumption. apply radix_gt_1. rewrite ulp_neq_0; try assumption. replace (FtoR beta f) with (F2R (Float beta (Pff.Fnum f) (Pff.Fexp f))). rewrite <- pff_canonic_is_canonic; try assumption. simpl; rewrite CanonicFulp; try assumption. unfold FtoR; simpl; rewrite bpow_powerRZ; ring. apply radix_gt_1. replace 1 with (Z.abs_nat 1) by easy. apply Zabs_nat_lt; lia. unfold F2R, FtoR; simpl. rewrite bpow_powerRZ; easy. Qed.
imports: Coq(Lia) Pff Core