proposition: Theorem radixRangeBoundExp : forall p q : float, Fcanonic radix b p -> Fcanonic radix b q -> (0 <= p)%R -> (p < q)%R -> (q < radix * p)%R -> Fexp p = Fexp q \/ Z.succ (Fexp p) = Fexp q.
proof: Proof. intros p q H' H'0 H'1 H'2 H'3. case (FcanonicLtPos _ radixMoreThanOne b precision) with (p := p) (q := q); auto with arith. 2: intros H'4; elim H'4; intros H'5 H'6; clear H'4; auto. intros H'4; right. Casec H'; intros H'. case (FcanonicLtPos _ radixMoreThanOne b precision) with (p := q) (q := Float (Fnum p) (Z.succ (Fexp p))); auto with arith. left. case H'; intros H1 H2; red in H1. repeat split; simpl in |- *; auto with zarith. apply Rle_trans with (FtoRradix p); auto; apply Rlt_le; auto. unfold FtoR in |- *; simpl in |- *. rewrite powerRZ_Zs; auto with real zarith; auto. rewrite <- Rmult_assoc; rewrite (fun (x : R) (y : Z) => Rmult_comm x y); rewrite Rmult_assoc; auto. apply IZR_neq; lia. simpl in |- *; intros; apply Zle_antisym; auto with zarith. simpl in |- *; auto. intros H'5; elim H'5; intros H'6 H'7; auto. case (FcanonicLtPos _ radixMoreThanOne b precision) with (p := q) (q := Float (nNormMin radix precision) (Z.succ (Fexp p))); auto with arith. left; repeat split; simpl in |- *. rewrite Z.abs_eq; auto with zarith. apply ZltNormMinVnum; auto with zarith. unfold nNormMin in |- *; apply Zpower_NR0; auto with zarith. apply Z.le_trans with (Fexp p); auto with zarith; apply H'. case H'; auto. rewrite <- (PosNormMin radix b precision); auto with zarith. apply Rle_trans with (1 := H'1); auto with real. apply Rlt_trans with (1 := H'3). unfold FtoR in |- *; simpl in |- *. rewrite powerRZ_Zs; auto with real zarith; auto. rewrite <- Rmult_assoc; rewrite (fun (x : R) (y : Z) => Rmult_comm x y); rewrite Rmult_assoc; auto. apply Rmult_lt_compat_l; auto with real arith. apply IZR_lt; lia. case H'. intros H'5 H'6; elim H'6; intros H'7 H'8; rewrite H'7; clear H'6. change (p < firstNormalPos radix b precision)%R in |- *. apply (FsubnormalLtFirstNormalPos radix); auto with arith. apply IZR_neq; lia. simpl in |- *; intros; apply Zle_antisym; auto with zarith. intros H'5; elim H'5; intros H'6 H'7; rewrite H'6; clear H'5; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz