diff --git a/theories/exp.v b/theories/exp.v
index cb7d2b8b7..d0e2a1ed8 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -624,7 +624,7 @@ Implicit Types x : R.
 
 Notation exp := (@expR R).
 
-Definition ln x : R := [get y | exp y == x ].
+Definition ln x : R := [get y | exp y == x ]. (*is this computable? *)
 
 Fact ln0 x : x <= 0 -> ln x = 0.
 Proof.
@@ -996,7 +996,7 @@ Implicit Types (s r : R) (x y : \bar R).
 Definition poweR x r :=
   match x with
   | x'%:E => (x' `^ r)%:E
-  | +oo => if r == 0%R then 1%E else +oo
+  | +oo => if r == 0%R then 1%E else if (r < 0)%R then 0 else +oo
   | -oo => if r == 0%R then 1%E else 0%E
   end.
 
@@ -1005,38 +1005,81 @@ Local Notation "x `^ r" := (poweR x r).
 Lemma poweR_EFin s r : s%:E `^ r = (s `^ r)%:E.
 Proof. by []. Qed.
 
+Lemma ltxy_ltyx s r : (s < r)%R -> (r < s)%R -> False.
+Proof.
+  by move/(@lt_trans _ _ r s s); rewrite ltxx falseE.
+Qed.
+
+Lemma poweRyr_lt0r r : (0 < r)%R -> +oo `^ r = +oo.
+Proof. 
+  move => pr; rewrite //= [_ == _](contra_neqF _ (lt0r_neq0 pr)); 
+    last apply /eqP. case : ifP => //=.
+    move => r0. exfalso; apply (ltxy_ltyx pr r0).
+Qed.
+
+Lemma poweRyr_ltr0 r : (r < 0)%R -> +oo `^ r = 0.
+Proof. by move => r0; rewrite //= [_ == _](contra_neqF _ (ltr0_neq0 r0)); 
+    last apply /eqP; rewrite r0.
+Qed.
+
+(*
 Lemma poweRyr r : r != 0%R -> +oo `^ r = +oo.
-Proof. by move/negbTE => /= ->. Qed.
+Proof. 
+  move/negbTE => /= ->. 
+  Qed.
+*)
 
 Lemma poweRe0 x : x `^ 0 = 1.
 Proof. by move: x => [x'| |]/=; rewrite ?powRr0// eqxx. Qed.
 
 Lemma poweRe1 x : 0 <= x -> x `^ 1 = x.
 Proof.
-by move: x => [x'| |]//= x0; rewrite ?powRr1// (negbTE (oner_neq0 _)).
+  move: x => [x'| |]//= x0; rewrite ?powRr1 //=.
+  rewrite (negbTE (oner_neq0 _)).
+  case : ifP => r0 //=. exfalso; apply (ltxy_ltyx r0 lte01).
 Qed.
 
 Lemma poweRN x r : x \is a fin_num -> x `^ (- r) = (fine x `^ r)^-1%:E.
 Proof. by case: x => // x xf; rewrite poweR_EFin powRN. Qed.
 
+
 Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0.
 Proof. by move=> r0 /=; rewrite (negbTE r0). Qed.
 
+
 Lemma poweR_eqy x r : x `^ r = +oo -> x = +oo.
 Proof. by case: x => [x| |] //=; case: ifP. Qed.
 
+Lemma eqy_poweR_lt0r x r : (0 < r)%R -> x = +oo -> x `^ r = +oo.
+Proof.
+  move: x => [| |]//= r0 _. rewrite gt_eqF //=.
+  case : ifP => f0 //=. exfalso; apply (ltxy_ltyx r0 f0).
+Qed. 
+(*
 Lemma eqy_poweR x r : (0 < r)%R -> x = +oo -> x `^ r = +oo.
 Proof. by move: x => [| |]//= r0 _; rewrite gt_eqF. Qed.
+*)
 
 Lemma poweR_lty x r : x < +oo -> x `^ r < +oo.
 Proof.
 by move: x => [x| |]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry.
 Qed.
 
+Lemma lty_poweRy_lt0r x r : (0 < r)%R -> x `^ r < +oo -> x < +oo.
+Proof.
+  move : x => [s | | ] //=; 
+    rewrite ?ltry//.
+  case : ifP; move/eqP => r0; 
+    first by rewrite r0 [(_ < _)%R]ltxx.
+    by case : ifP => //=; move/ltxy_ltyx => //=.
+Qed.
+
+(*
 Lemma lty_poweRy x r : r != 0%R -> x `^ r < +oo -> x < +oo.
 Proof.
 by move=> r0; move: x => [x| | _]//=; rewrite ?ltry// (negbTE r0).
 Qed.
+*)
 
 Lemma poweR0r r : r != 0%R -> 0 `^ r = 0.
 Proof. by move=> r0; rewrite poweR_EFin powR0. Qed.
@@ -1045,16 +1088,32 @@ Lemma poweR1r r : 1 `^ r = 1. Proof. by rewrite poweR_EFin powR1. Qed.
 
 Lemma fine_poweR x r : fine (x `^ r) = ((fine x) `^ r)%R.
 Proof.
-by move: x => [x| |]//=; case: ifPn => [/eqP ->|?]; rewrite ?powRr0 ?powR0.
+  move: x => [x| |]//=.
+  case : ifP => [/eqP -> |r0]; rewrite ?powRr0 //= (powR0 (contraFneq _ r0)); 
+    last by move/eqP => //=.
+  - case : ifP => //=.
+  - case : ifP => [/eqP -> //= | r0]; rewrite ?powRr0 //= ?powR0 //=;
+    by rewrite (contraFneq _ r0); last by move/eqP => //=. 
 Qed.
 
 Lemma poweR_ge0 x r : 0 <= x `^ r.
-Proof. by move: x => [x| |]/=; rewrite ?lee_fin ?powR_ge0//; case: ifPn. Qed.
+Proof.
+  move: x => [x| |]/=; rewrite ?lee_fin ?powR_ge0//; 
+  repeat case : ifP => //=. 
+Qed.
+
+Lemma poweR_gt0 x r : 0 < x < +oo -> 0 < x `^ r.
+Proof.
+  move: x => [x /andP [x0 xy]| /andP [x0 xy]|]//=.
+  move : x0; repeat apply lte_tofin; apply powR_gt0.
+Qed.
 
+(*
 Lemma poweR_gt0 x r : 0 < x -> 0 < x `^ r.
 Proof.
 by move: x => [x|_|]//=; [rewrite lte_fin; exact: powR_gt0|case: ifPn].
 Qed.
+*)
 
 Lemma gt0_poweR x r : (0 < r)%R -> 0 <= x -> 0 < x `^ r -> 0 < x.
 Proof.
@@ -1062,25 +1121,44 @@ move=> r0; move: x => [x|//|]; rewrite ?leeNe_eq// lee_fin !lte_fin.
 exact: gt0_powR.
 Qed.
 
+Lemma poweR_eq0 x r : 0 <= x < +oo -> (x `^ r == 0) = ((x == 0) && (r != 0%R)).
+Proof.
+  move: x => [x _|/= /andP [_ ]|//]; 
+  first by rewrite poweR_EFin eqe powR_eq0.
+  by rewrite ltxx.
+Qed.
+
+(*
 Lemma poweR_eq0 x r : 0 <= x -> (x `^ r == 0) = ((x == 0) && (r != 0%R)).
 Proof.
 move: x => [x _|_/=|//]; first by rewrite poweR_EFin eqe powR_eq0.
 by case: ifP => //; rewrite onee_eq0.
 Qed.
+*)
 
+Lemma poweR_eq0_eq0 x r : 0 <= x < +oo -> x `^ r = 0 -> x = 0.
+Proof.
+  by move=> + /eqP => /poweR_eq0-> /andP[/eqP].
+Qed.
+(*
 Lemma poweR_eq0_eq0 x r : 0 <= x -> x `^ r = 0 -> x = 0.
 Proof. by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed.
+*)
 
 Lemma gt0_ler_poweR r : (0 <= r)%R ->
   {in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}.
 Proof.
 move=> r0 + y; case=> //= [x /[1!in_itv]/= /andP[xint _]| _ _].
-- case: y => //= [y /[1!in_itv]/= /andP[yint _] xy| _ _].
-  + by rewrite !lee_fin ge0_ler_powR.
-  + by case: eqP => [->|]; rewrite ?powRr0 ?leey.
-- by rewrite leye_eq => /eqP ->.
+- case: y => //= [y /[1!in_itv]/= /andP[yint _] xy| _ _]; 
+    first by rewrite !lee_fin ge0_ler_powR.
+  case : ifP => /eqP H; rewrite ?H //= ?powRr0 //=; case : ifP => //= H0. 
+    - rewrite le0r in r0; case : (orP r0) => //= /eqP => //=; 
+        first by move => H1; exfalso; apply (ltxy_ltyx H0 (eqP H1)).
+    - apply (@leey _ (x `^ r)%:E). 
+- case : y => //=.
 Qed.
 
+
 Lemma fin_num_poweR x r : x \is a fin_num -> x `^ r \is a fin_num.
 Proof.
 by move=> xfin; rewrite ge0_fin_numE ?poweR_lty ?ltey_eq ?xfin// poweR_ge0.