proposition: Theorem Fcanonic_Rle_Zle : forall x y : float, Fcanonic x -> Fcanonic y -> (Rabs x <= Rabs y)%R -> (Fexp x <= Fexp y)%Z.
proof: Proof. intros x y H H0 H1. cut (forall z : float, Fexp z = Fexp (Fabs z) :>Z); [ intros E | intros; unfold Fabs in |- *; simpl in |- *; auto with zarith ]. rewrite (E x); rewrite (E y). cut (Fcanonic (Fabs x)); [ intros D | apply FcanonicFabs; auto ]. cut (Fcanonic (Fabs y)); [ intros G | apply FcanonicFabs; auto ]. case H1; intros Z2. case (FcanonicLtPos (Fabs x) (Fabs y)); auto with zarith. rewrite (Fabs_correct radix); auto with real zarith. apply Rabs_pos. repeat rewrite (Fabs_correct radix); auto with real zarith. rewrite (FcanonicUnique (Fabs x) (Fabs y)); auto with zarith. repeat rewrite (Fabs_correct radix); auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz