proposition: Theorem FcanonicNegFexpRlt : forall x y : float, (x <= 0)%R -> (y <= 0)%R -> Fcanonic x -> Fcanonic y -> (Fexp x < Fexp y)%Z -> (y < x)%R.
proof: Proof. intros x y H' H'0 H'1 H'2 H'3. case (Rle_or_lt x y); auto. intros H'4; case H'4; clear H'4; intros H'4. case FcanonicLtNeg with (p := x) (q := y); auto. intros H'5; contradict H'3; auto with zarith. intros H'5; elim H'5; intros H'6 H'7; clear H'5; contradict H'3; rewrite H'6; auto with zarith. contradict H'3. rewrite FcanonicUnique with (p := x) (q := y); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz