proposition: Theorem FsubnormalnormalLtPos : forall p q : float, Fsubnormal p -> Fnormal q -> (0 <= p)%R -> (0 <= q)%R -> (p < q)%R.
proof: Proof. intros p q H' H'0 H'1 H'2. apply Rlt_le_trans with (r2 := FtoRradix firstNormalPos). apply FsubnormalLtFirstNormalPos; auto. apply FnormalLtFirstNormalPos; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz