proposition: Theorem LSBMinus : forall p q : float, ~ is_Fzero (Fminus radix p q) -> (Z.min (LSB radix p) (LSB radix q) <= LSB radix (Fminus radix p q))%Z.
proof: Proof. intros p q H'1. elim (LSB_rep_min radix) with (p := p); auto; intros z E. elim (LSB_rep_min radix) with (p := q); auto; intros z0 E0. replace (LSB radix (Fminus radix p q)) with (LSB radix (Fminus radix (Float z (LSB radix p)) (Float z0 (LSB radix q)))). replace (Z.min (LSB radix p) (LSB radix q)) with (Fexp (Fminus radix (Float z (LSB radix p)) (Float z0 (LSB radix q)))); [ idtac | simpl in |- *; auto ]. apply Fexp_le_LSB; auto. apply sym_equal; apply LSB_comp; auto. repeat rewrite Fminus_correct; auto with arith. unfold FtoRradix in E; unfold FtoRradix in E0; rewrite E; rewrite E0; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz