proposition: Theorem FsubnormalnormalLtNeg : forall p q : float, Fsubnormal p -> Fnormal q -> (p <= 0)%R -> (q <= 0)%R -> (q < p)%R.
proof: Proof. intros p q H' H'0 H'1 H'2. rewrite <- (Ropp_involutive p); rewrite <- (Ropp_involutive q). apply Ropp_gt_lt_contravar; red in |- *. unfold FtoRradix in |- *; repeat rewrite <- Fopp_correct. apply FsubnormalnormalLtPos; auto. apply FsubnormFopp; auto. apply FnormalFop; auto. unfold FtoRradix in |- *; rewrite Fopp_correct; replace 0%R with (-0)%R; auto with real. unfold FtoRradix in |- *; rewrite Fopp_correct; replace 0%R with (-0)%R; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz