proposition: Theorem FsubnormalLt : forall p q : float, Fsubnormal p -> Fsubnormal q -> (p < q)%R -> (Fnum p < Fnum q)%Z.
proof: Proof. intros p q H' H'0 H'1. apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith. apply trans_equal with (- dExp b)%Z. case H'; auto. intros H1 H2; case H2; auto. apply sym_equal; case H'0; auto. intros H1 H2; case H2; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz