proposition: Theorem FcanonicLtPos : forall p q : float, Fcanonic p -> Fcanonic q -> (0 <= p)%R -> (p < q)%R -> (Fexp p < Fexp q)%Z \/ Fexp p = Fexp q /\ (Fnum p < Fnum q)%Z.
proof: Proof. intros p q H' H'0 H'1 H'2; case H'; case H'0. intros H'3 H'4; apply FnormalLtPos; auto. intros H'3 H'4; absurd (p < q)%R; auto. apply Rlt_asym. apply FsubnormalnormalLtPos; auto. apply Rle_trans with (r2 := FtoRradix p); auto with real. intros H'3 H'4; case (Z.eq_dec (Fexp q) (- dExp b)); intros H'5. right; split. rewrite H'5; case H'4; intros H1 H2; case H2; auto. apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith. rewrite H'5; case H'4; intros H1 H2; case H2; auto. left. replace (Fexp p) with (- dExp b)%Z; [ idtac | apply sym_equal, H'4 ]. case (Zle_lt_or_eq (- dExp b) (Fexp q)); try apply H'3; auto with zarith. intros H'3 H'4; right; split. apply trans_equal with (- dExp b)%Z; try apply H'4. apply sym_equal, H'3. apply FsubnormalLt; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz