Add lemmas used by RefinedRust

This MR adds lemmas that RefinedRust uses in its model of lifetime contexts.

Since the lifetime logic is now a separate opam package, this would allow us to use that package instead of maintaining a fork of lambda-rust.

lifetime/model/creation.v

@@ -184,4 +184,27 @@ Proof.
       eapply HK'', Hκ. rewrite elem_of_union. auto.
     + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
 Qed.
+
+(* TODO: remove once stdpp!562 is merged *)
+Lemma lower_bound_exists `{FinSet A C} R `{!Transitive R,
+    ∀ x y, Decision (R x y)} `{!Inhabited A} (X : C) :
+  ∃ x, minimal R x X.
+Proof.
+  destruct (set_choose_or_empty X) as [ (y & Ha) | Hne].
+  - edestruct (minimal_exists R X) as (x & Hel & Hmin); first set_solver.
+    exists x. done.
+  - exists inhabitant. intros y Hel. set_solver.
+Qed.
+Lemma lft_fresh_strong κ κ' :
+  ∃ i : positive, ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
+Proof.
+  unfold meet, lft_intersect.
+  destruct (lower_bound_exists (flip Pos.le) (dom κ)) as (i & Ha).
+  exists (i + 1)%positive.
+  intros k Hik Heq. subst κ.
+  ospecialize (Ha k _ _); simpl in *; [ | lia..].
+  apply gmultiset_elem_of_dom.
+  apply gmultiset_elem_of_disj_union.
+  left. by apply gmultiset_elem_of_singleton.
+Qed.
 End creation.