proposition: Theorem MinOrMax2 : forall (z : R) (p : float), Fbounded b p -> Fcanonic radix b p -> (0 < p)%R -> (Rabs (z - p) < Fulp b radix precision p)%R -> (p <= z)%R -> MinOrMax z p.
proof: Proof. intros z p Hp1 Hp2 H H1 H2. unfold MinOrMax in |- *; left; unfold isMin in |- *. split; auto; split; auto. intros f Hf H3. replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f)); [ idtac | apply FnormalizeCorrect; auto with zarith arith ]. replace p with (FPred b radix precision (FSucc b radix precision p)); [ idtac | apply FPredSuc; auto with zarith arith ]. apply FPredProp; auto with zarith arith. apply FnormalizeCanonic; auto with arith zarith. apply FSuccCanonic; auto with arith zarith. apply Rle_lt_trans with z. rewrite FnormalizeCorrect; auto with arith zarith. apply Rlt_le_trans with (FtoRradix p + Fulp b radix precision p)%R. apply Rplus_lt_reg_r with (- FtoRradix p)%R. ring_simplify. apply Rle_lt_trans with (2 := H1); right. rewrite Rabs_right; try ring. apply Rle_ge; apply Rplus_le_reg_l with (FtoRradix p); auto with real. ring_simplify; auto with real. pattern p at -3 in |- *; replace p with (FPred b radix precision (FSucc b radix precision p)); [ idtac | apply FPredSuc; auto with zarith arith ]. unfold FtoRradix in |- *; rewrite FpredUlpPos with (x := FSucc b radix precision p); auto with zarith arith real. apply FSuccCanonic; auto with zarith arith. apply Rlt_trans with (FtoRradix p); auto with real. unfold FtoRradix in |- *; apply FSuccLt; auto with zarith real. Qed.
imports: Reals ZArith List PeanoNat Psatz