proposition: Theorem FcanonicLtNeg : forall p q : float, Fcanonic p -> Fcanonic q -> (q <= 0)%R -> (p < q)%R -> (Fexp q < Fexp p)%Z \/ Fexp p = Fexp q /\ (Fnum p < Fnum q)%Z.
proof: Proof. intros p q H' H'0 H'1 H'2. cut ((Fexp (Fopp q) < Fexp (Fopp p))%Z \/ Fexp (Fopp q) = Fexp (Fopp p) /\ (Fnum (Fopp q) < Fnum (Fopp p))%Z). simpl in |- *. intros H'3; elim H'3; clear H'3; intros H'3; [ idtac | elim H'3; clear H'3; intros H'3 H'4 ]; auto; right; split; auto with zarith. apply FcanonicLtPos; try apply FcanonicFopp; auto; unfold FtoRradix in |- *; repeat rewrite Fopp_correct; replace 0%R with (-0)%R; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz