proposition: Theorem eqExpLess : forall (b : Fbound) (p q : float), Fbounded b p -> p = q :>R -> exists r : float, Fbounded b r /\ r = q :>R /\ (Fexp q <= Fexp r)%R.
proof: Proof. intros b p q H' H'0. case (Rle_or_lt (Fexp q) (Fexp p)); intros H'1. exists p; repeat (split; auto). exists q; split; [ idtac | split ]; auto with real. apply FboundedEqExp with (p := p); auto. apply Rlt_le; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz