Library zoo.iris.base_logic.lib.cinv

Require Export iris.base_logic.lib.cancelable_invariants.

Require Import zoo.prelude.
Require Import zoo.common.math.
Require Import zoo.iris.bi.big_op.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Section cinv۰G.
  Context `{inv۰G : !invGS Σ}.
  Context `{cinv۰G : !cinvG Σ}.

  Lemma cinv_ownｰdivide {γ q} n :
    n ≠ 0 →
    cinv_own γ q ⊢
    [∗ list] _ ∈ seq 0 n, cinv_own γ (q / Qp۰of_nat n).
  Lemma cinv_ownｰgather γ q n :
    n ≠ 0 →
    ([∗ list] _ ∈ seq 0 n, cinv_own γ (q / Qp۰of_nat n)) ⊢
    cinv_own γ q.
End cinv۰G.