proposition: Lemma max_valid_ub x y : F.valid_ub x = true -> F.valid_ub y = true -> (F.valid_ub (F.max x y) = true /\ F.toX (F.max x y) = Xmax (F.toX x) (F.toX y)).
proof: Proof. rewrite !F.valid_ub_correct. generalize (F.max_correct x y). generalize (F.classify_correct x) ; rewrite F.real_correct ; case_eq (F.classify x); intro Cx ; [..|easy|] ; [case_eq (F.toX x); [easy|] ; intros rx Hx _ |case_eq (F.toX x); [|easy] ; intros Hx _..] ; ( generalize (F.classify_correct y) ; rewrite F.real_correct ; case_eq (F.classify y); intro Cy ; [..|easy|] ; [case_eq (F.toX y); [easy|] ; intros ry Hy _ |case_eq (F.toX y); [|easy] ; intros Hy _..] ) ; intros Hmax _ _ ; generalize (F.classify_correct (F.max x y)) ; rewrite F.real_correct ; rewrite Hmax ; simpl ; rewrite ?Cx, ?Cy ; rewrite ?Hx, ?Hy ; [case F.classify ; easy|..] ; now case F.toX. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic