proposition: Theorem FnormalLtPos : forall p q : float, Fnormal p -> Fnormal 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 (Zle_or_lt (Fexp q) (Fexp p)); auto. intros H'3; right. case (Zle_lt_or_eq _ _ H'3); intros H'4. 2: split; auto. 2: apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith. absurd (Fnum (Fshift radix (Z.abs_nat (Fexp p - Fexp q)) p) < Fnum q)%Z; auto. 2: apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith. 2: unfold FtoRradix in |- *; rewrite FshiftCorrect; auto. 2: unfold Fshift in |- *; simpl in |- *; lia. red in |- *; intros H'5. absurd (Fdigit radix (Fshift radix (Z.abs_nat (Fexp p - Fexp q)) p) <= Fdigit radix q); auto with arith. rewrite FshiftFdigit; auto with arith. replace (Fdigit radix p) with precision. replace (Fdigit radix q) with precision; try lia. now apply sym_equal, FnormalPrecision. now apply sym_equal, FnormalPrecision. apply FnormalNotZero; auto with arith. unfold Fdigit in |- *; apply digit_monotone; auto with arith. repeat rewrite Z.abs_eq; auto with zarith. apply LeR0Fnum with (radix := radix); auto with zarith. apply Rle_trans with (r2 := FtoRradix p); auto with real. apply LeR0Fnum with (radix := radix); auto with zarith. unfold FtoRradix in |- *; rewrite FshiftCorrect; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz