Library zoo.iris.base_logic.lib.cinv

From iris.base_logic Require Export
  lib.cancelable_invariants.

From zoo Require Import
  prelude.
From zoo.common Require Import
  math.
From zoo.iris.bi Require Import
  big_op.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  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.