proposition: Theorem MinOrMax3 : forall (z : R) (p : float), Fbounded b p -> Fcanonic radix b p -> 0%R = p -> (Rabs (z - p) < Fulp b radix precision (FPred b radix precision p))%R -> MinOrMax z p.
proof: Proof. intros z p Hp Hcan Hzero. replace (z - FtoRradix p)%R with z; [ idtac | rewrite <- Hzero; ring ]. case (Rcase_abs z); intros H1; [ rewrite Rabs_left | rewrite Rabs_right ]; auto; intros H. apply MinOrMax3_aux; auto with real. apply MinOrMax_Fopp. apply MinOrMax3_aux; auto with real. apply oppBounded; easy. apply FcanonicFopp; easy. unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real. rewrite Ropp_involutive. replace (Fopp p) with p; auto. apply floatEq; auto; simpl in |- *. cut (is_Fzero p); [ unfold is_Fzero in |- *; intros H2; repeat rewrite H2 | apply is_Fzero_rep2 with radix ]; auto with zarith real. Qed.
imports: Reals ZArith List PeanoNat Psatz