proposition: Lemma tLe: (Rabs t <= powerRZ radix (Fexp z)*(radix+1))%R.
proof: Proof. replace (FtoRradix t) with (uh-z)%R. replace (uh-z)%R with ((a*x+b-z)+(-(a*x-ph)+-((ph+b)-uh)))%R;[idtac|ring]. apply Rle_trans with (Rabs (a*x+b-z)+Rabs ( - (a * x - ph) + - (ph + b - uh)))%R; [apply Rabs_triang|idtac]. apply Rle_trans with (powerRZ radix (Fexp z)+powerRZ radix (Fexp z)*radix)%R;[idtac|right; ring]. apply Rplus_le_compat. apply Rle_trans with (Fulp bo radix p z). apply Rlt_le; unfold FtoRradix; apply RoundedModeUlp with (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. rewrite CanonicFulp; auto with zarith;[unfold FtoR; simpl; right; ring|left; auto]. apply Rle_trans with (powerRZ radix (Fexp z+1)); [idtac|rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; right; ring]. apply Rle_trans with (Rabs (-(a*x-ph))+Rabs (-(ph+b-uh)))%R;[apply Rabs_triang|idtac]. rewrite Rabs_Ropp; rewrite Rabs_Ropp. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (powerRZ radix (Fexp ph)+powerRZ radix (Fexp uh))%R; [idtac|apply LeExp]. apply Rle_trans with (2*Rabs (a*x-ph)+2*Rabs (ph+b-uh))%R;[simpl; right; ring|idtac]. apply Rplus_le_compat. apply Rle_trans with (Fulp bo radix p ph). unfold FtoRradix; apply ClosestUlp; auto with zarith. rewrite CanonicFulp; auto with zarith;[unfold FtoR; simpl; right; ring|left; auto]. apply Rle_trans with (Fulp bo radix p uh). unfold FtoRradix; apply ClosestUlp; auto with zarith. rewrite CanonicFulp; auto with zarith;[unfold FtoR; simpl; right; ring|left; auto]. elim tBounded with bo radix p a x b ph pl uh z; auto with zarith. fold FtoRradix; intros t' T; elim T; intros; clear T. rewrite <- H0; unfold FtoRradix. apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; rewrite H0; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz