proposition: Lemma Fround_at_prec_pos_Eq : forall beta mode prec (x : ufloat beta), ufloat_pos_Eq beta x -> FtoX (Fround_at_prec mode prec x) = Xround beta mode prec (UtoX x).
proof: Proof. Proof with auto with typeclass_instances. intros beta mode prec [| |s m e [| | |]] H ; try elim H ; clear H. apply refl_equal. simpl. unfold round. rewrite round_0... unfold Xround, UtoX. rewrite FtoR_split. replace (F2R (Defs.Float beta (cond_Zopp s (Zpos m)) e)) with (if s then Ropp (F2R (Defs.Float beta (Zpos m) e)) else F2R (Defs.Float beta (Zpos m) e)). apply Fround_at_prec_correct. now apply F2R_gt_0. now constructor. easy. rewrite <- F2R_opp. now case s. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic