proposition: Theorem NormalAndSubNormalNotEq : forall p q : float, Fnormal p -> Fsubnormal q -> p <> q :>R.
proof: Proof. intros p q H' H'0; red in |- *; intros H'1. case (Rtotal_order 0 p); intros H'2. absurd (q < p)%R. rewrite <- H'1; auto with real. apply FsubnormalnormalLtPos; auto with real. rewrite <- H'1; auto with real. absurd (p < q)%R. rewrite <- H'1; auto with real. apply FsubnormalnormalLtNeg; auto with real. rewrite <- H'1; auto with real. elim H'2; intros H'3; try rewrite <- H'3; auto with real. elim H'2; intros H'3; try rewrite <- H'3; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz