proposition: Theorem Fmax_correct : forall beta (x y : float beta), FtoX (Fmax x y) = Xmax (FtoX x) (FtoX y).
proof: Proof. intros. unfold Fmax, Rmax. rewrite (Fcmp_correct beta x y). case_eq (FtoX x) ; [ split | intros xr Hx ]. case_eq (FtoX y) ; [ split | intros yr Hy ]. simpl. destruct (Rle_dec xr yr) as [[H|H]|H]. rewrite Rcompare_Lt. exact Hy. exact H. now rewrite Rcompare_Eq. rewrite Rcompare_Gt. exact Hx. apply Rnot_le_lt with (1 := H). Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic