proposition: Theorem RleFexpFabs : forall p : float, p <> 0%R :>R -> (Float 1 (Fexp p) <= Fabs p)%R.
proof: Proof. intros p H'. unfold FtoRradix, FtoR, Fabs in |- *; simpl in |- *. apply Rmult_le_compat_r; auto with real arith. now apply powerRZ_le, IZR_lt. rewrite Zabs_absolu. apply IZR_le. cut (Z.abs_nat (Fnum p) <> 0); auto with zarith. contradict H'. unfold FtoRradix, FtoR in |- *; simpl in |- *. replace (Fnum p) with 0%Z; try (simpl;ring). generalize H'; case (Fnum p); simpl in |- *; auto with zarith arith; intros p0 H'3; contradict H'3; auto with zarith arith; apply convert_not_O. Qed.
imports: Reals ZArith List PeanoNat Psatz