"Exponentiation" for separating conjunctions
Sometimes it makes sense to have a statement about possessing n
copies of the same resource. For example (in pseudocode), own γ 1%Qp -∗ (own γ (1/n))^n
. Maybe such an operation should be available in the standard library, along with some useful lemmas about exponentiation?
An example of what exponentiation could be defined as:
Fixpoint iPropPow {Σ} (R : iProp Σ) (n : nat) : iProp Σ :=
match n with
| 0 => (True)%I
| S n' => (R ∗ iPropPow R n')%I
end.