Merge PR #11362: Lia bugfix 11191

Reviewed-by: maximedenes

1 files changed, 19 insertions, 0 deletions

diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v
index 97f6fe0613..edfb5a2a94 100644
--- a/plugins/micromega/ZifyInst.v
+++ b/plugins/micromega/ZifyInst.v
@@ -523,3 +523,22 @@ Instance SatProdPos : Saturate Z.mul :=
     SatOk := Z.mul_pos_pos
   |}.
 Add Saturate SatProdPos.
+
+Lemma pow_pos_strict :
+  forall a b,
+    0 < a -> 0 < b -> 0 < a ^ b.
+Proof.
+  intros.
+  apply Z.pow_pos_nonneg; auto.
+  apply Z.lt_le_incl;auto.
+Qed.
+
+
+Instance SatPowPos : Saturate Z.pow :=
+  {|
+    PArg1 := fun x => 0 < x;
+    PArg2 := fun y => 0 < y;
+    PRes  := fun r => 0 < r;
+    SatOk := pow_pos_strict
+  |}.
+Add Saturate SatPowPos.