proposition: Theorem FcanonicLeastExp : forall x y : float, x = y :>R -> Fbounded b x -> Fcanonic y -> (Fexp y <= Fexp x)%Z.
proof: Proof. intros x y H H0 H1. cut (Fcanonic (Fnormalize x)); [ intros | apply FnormalizeCanonic; auto ]. replace y with (Fnormalize x); [ simpl in |- * | apply FcanonicUnique; auto with real ]. unfold Fnormalize in |- *. case (Z_zerop (Fnum x)); simpl in |- *; intros Z1; try apply H0. apply Zplus_le_reg_l with (- Fexp x)%Z. replace (- Fexp x + Fexp x)%Z with (- (0))%Z; try ring. replace (- Fexp x + (Fexp x - min (precision - Fdigit radix x) (Z.abs_nat (dExp b + Fexp x))))%Z with (- min (precision - Fdigit radix x) (Z.abs_nat (dExp b + Fexp x)))%Z; try ring. apply Zle_Zopp; auto with arith zarith. rewrite <- H. apply FnormalizeCorrect. Qed.
imports: Reals ZArith List PeanoNat Psatz