proposition: Theorem MinOrMax3_aux : forall (z : R) (p : float), Fbounded b p -> Fcanonic radix b p -> 0%R = p -> (z <= 0)%R -> (- z < Fulp b radix precision (FPred b radix precision p))%R -> MinOrMax z p.
proof: Proof. intros z p Hp Hcan Hzero H. right; unfold isMax in |- *. fold FtoRradix in |- *; rewrite <- Hzero. split; auto; split; auto with real. intros f Hf H2. unfold FtoRradix in |- *; replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f)); [ idtac | apply FnormalizeCorrect; auto with zarith arith ]. cut (Fcanonic radix b (Fzero (- dExp b))); [ intros H3 | idtac ]. 2: right; repeat (split; simpl in |- *; rewrite ?Zmult_0_r; auto with zarith). cut (p = Fzero (- dExp b)); [ intros H4 | idtac ]. 2: apply FcanonicUnique with (radix := radix) (precision := precision) (b := b); auto with zarith. 2: fold FtoRradix in |- *; rewrite <- Hzero; auto with real. 2: unfold FtoRradix in |- *; apply sym_eq; apply FzeroisZero. cut (0 < pPred (vNum b))%Z; [ intros V | apply pPredMoreThanOne with radix precision; auto with zarith ]. cut (1 < Zpos (vNum b))%Z; [ intros V' | apply vNumbMoreThanOne with radix precision; auto with zarith ]. replace 0%R with (FtoR radix (FSucc b radix precision (FPred b radix precision (Fzero (- dExp b))))). apply FSuccProp; auto with zarith arith. apply FPredCanonic; auto with arith zarith. apply FnormalizeCanonic; auto with arith zarith. apply Rlt_le_trans with z. 2: rewrite FnormalizeCorrect; auto with arith zarith. apply Ropp_lt_cancel; apply Rlt_le_trans with (1 := H0). rewrite H4; right. rewrite FPredSimpl4; simpl in |- *; auto with zarith. 2: unfold nNormMin in |- *; auto with zarith. unfold Fulp in |- *. replace (Fnormalize radix b precision (Float (-1) (- dExp b))) with (Float (-1) (- dExp b)); [ unfold FtoRradix, FtoR in |- *; simpl in |- *; ring | idtac ]. apply FcanonicUnique with (radix := radix) (precision := precision) (b := b); auto with zarith. right; repeat (split; simpl in |- *; auto with zarith). rewrite pGivesBound. rewrite <- Zabs_Zopp; rewrite Z.abs_eq; auto with zarith. replace (- (radix * -1))%Z with (Zpower_nat radix 1); auto with arith zarith. apply Zpower_nat_monotone_lt; lia. unfold Zpower_nat in |- *; simpl in |- *; ring. apply FnormalizeCanonic; auto with zarith. repeat (split; simpl in |- *; auto with zarith). apply sym_eq; apply FnormalizeCorrect; auto with zarith. now apply Z.lt_neq, Zpower_nat_less. rewrite FPredSimpl4; simpl in |- *; auto with zarith. rewrite FSuccSimpl4; simpl in |- *; auto with zarith. simpl in |- *; unfold FtoR in |- *; simpl in |- *; ring. unfold nNormMin in |- *. replace (-1)%Z with (- Zpower_nat radix (pred 1))%Z; auto with zarith arith. apply sym_not_eq, Z.lt_neq, Zlt_Zopp. apply Zpower_nat_monotone_lt; lia. now apply Z.lt_neq, Zpower_nat_less. Qed.
imports: Reals ZArith List PeanoNat Psatz