proposition: Lemma LeExp1: (Fexp ph <= Fexp uh+1)%Z.
proof: Proof. case (Zle_or_lt (Fexp ph) (Fexp uh+1)); auto with zarith; intros. absurd (FtoRradix ul=0); auto with real. rewrite ulDef; assert (FtoRradix uh=ph+b)%R; auto with real. unfold FtoRradix; apply plusExact2 with bo p; auto with real zarith. left; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz