proposition: Lemma Fulp_ulp: forall f, Fbounded 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. assert (Y1: (1 < beta)%Z) by apply radix_gt_1. assert (Y2:Z.abs_nat p <> 0). apply sym_not_eq, Nat.lt_neq. replace 0 with (Z.abs_nat 0) by easy. apply Zabs_nat_lt; lia. rewrite FulpComp with (q:=Fnormalize beta b (Z.abs_nat p) f); try assumption. rewrite <- FnormalizeCorrect with beta b (Z.abs_nat p) f; try assumption. apply Fulp_ulp_aux. apply FnormalizeCanonic; try assumption. replace 1 with (Z.abs_nat 1) by easy. apply Zabs_nat_lt; lia. apply FnormalizeBounded; try assumption. apply sym_eq, FnormalizeCorrect; try assumption. Qed.
imports: Coq(Lia) Pff Core