diff --git a/algebra/frac.v b/algebra/frac.v
index 4630dc973fcae8ba097e245e5fb74852afeb18d2..aeb1dfd92884844d17c1da6203b2a452300dab74 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -1,4 +1,4 @@
-From Coq Require Import Qcanon.
+From Coq.QArith Require Import Qcanon.
 From algebra Require Export cmra.
 From algebra Require Import functor upred.
 Local Arguments validN _ _ _ !_ /.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index b6d415b1480f96330ee568d9ccdef6595679d088..8888ae4c894072b137045c83972019eb30cdc0e7 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -132,6 +132,10 @@ Section heap.
     rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
   Qed.
 
+  Lemma heap_mapsto_op_split l q v :
+    (l ↦{q} v)%I ≡ (l ↦{q/2} v ★ l ↦{q/2} v)%I.
+  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
+
   (** Weakest precondition *)
   Lemma wp_alloc N E e v P Φ :
     to_val e = Some v →
@@ -145,7 +149,7 @@ Section heap.
     apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with I.
     rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc left_id discrete_valid; apply const_elim_sep_l=> ?.
+    rewrite -assoc left_id; apply const_elim_sep_l=> ?.
     rewrite -(wp_alloc_pst _ (of_heap h)) //.
     apply sep_mono_r; rewrite HP; apply later_mono.
     apply forall_mono=> l; apply wand_intro_l.
@@ -168,7 +172,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
       with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
+    rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
     rewrite const_equiv // left_id.
     rewrite /heap_inv of_heap_singleton_op //.
@@ -185,7 +189,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
       with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
+    rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
     rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
     rewrite const_equiv; last naive_solver.
@@ -202,7 +206,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
       with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10 with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
+    rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
     rewrite const_equiv // left_id.
     rewrite /heap_inv !of_heap_singleton_op //.
@@ -219,7 +223,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
       with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10 with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
+    rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) //;
       last by rewrite lookup_insert.
     rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 4ddaab82edfcdd1e51428d0e7e2e774eb95fbfef..6e379ddcf61b8197e8c2df4428e968e72cc15c85 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -101,15 +101,12 @@ Section auth.
 
   Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
 
-  (* Notice how the user has to prove that `bâ‹…a'` is valid at all
-     step-indices. However, since A is timeless, that should not be
-     a restriction. *)
   Lemma auth_fsa E N P (Ψ : V → iPropG Λ Σ) γ a :
     fsaV →
     nclose N ⊆ E →
     P ⊑ auth_ctx γ N φ →
     P ⊑ (▷ auth_own γ a ★ ∀ a',
-          ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
             ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
             (auth_own γ (L a) -★ Ψ x))) →
@@ -124,7 +121,7 @@ Section auth.
     apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
     rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]comm.
     eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
-    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc. done. }
+    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc discrete_valid.  done. }
     rewrite fsa_frame_l.
     apply (fsa_mono_pvs fsa)=> x.
     rewrite sep_exist_l; apply exist_elim=> L.
@@ -141,7 +138,7 @@ Section auth.
     nclose N ⊆ E →
     P ⊑ auth_ctx γ N φ →
     P ⊑ (▷ auth_own γ a ★ (∀ a',
-          ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x,
             ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
             (auth_own γ (L a) -★ Ψ x)))) →