proposition: Lemma pff_round_DN_is_round: forall (r:R), FtoR beta (RND_Min b beta (Z.abs_nat p) r) = round beta (FLT_exp (- dExp b) p) Zfloor r.
proof: Proof. Proof with auto with typeclass_instances. intros r. generalize (radix_gt_1 beta); intros M. assert (K:Valid_exp (FLT_exp (- dExp b) p)). apply FLT_exp_valid. unfold Prec_gt_0; auto with zarith. destruct (format_is_pff_format_can (round beta (FLT_exp (- dExp b) p) Zfloor r)) as (fd,(Hfd1,Hfd2)). apply generic_format_round... rewrite <- Hfd1. apply MinUniqueP with b r. apply RND_Min_correct; try assumption. apply Nat2Z.inj_lt; rewrite inj_abs; simpl; lia. split. apply FcanonicBound with (1:=Hfd2). assert (T:Rnd_DN_pt (generic_format beta (FLT_exp (- dExp b) p)) r (round beta (FLT_exp (- dExp b) p) Zfloor r)). apply round_DN_pt... destruct T as (T1,(T2,T3)). split. rewrite Hfd1; apply T2. intros g Hg1 Hg2. rewrite Hfd1; apply T3; try assumption. now apply pff_format_is_format. Qed.
imports: Coq(Lia) Pff Core