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,30 @@ Proof.
       eapply HK'', Hκ. rewrite elem_of_union. auto.
     + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
 Qed.
+
+(* TODO : move? *)
+Local Lemma fin_set_sup_positive {M} `{!Elements positive M} `{!ElemOf positive M}
+  `{!Empty M} `{!Singleton positive M}
+  `{!Union M} `{!Intersection M} `{!Difference M}
+  `{!FinSet positive M} (m : M) :
+  ∃ i : positive, ∀ k, k ∈ m → (k < i)%positive.
+Proof.
+  exists (Pos.succ (foldr Pos.max 1%positive (elements m))).
+  setoid_rewrite <-(elem_of_elements m). generalize (elements m) => l.
+  induction l as [ | n l IH]; simpl.
+  - intros ? []%elem_of_nil.
+  - intros ? [<- | H]%elem_of_cons; first lia.
+    apply IH in H. lia.
+Qed.
+Lemma lft_fresh_strong κ κ' :
+  ∃ i : positive, ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
+Proof.
+  unfold meet, lft_intersect.
+  destruct (fin_set_sup_positive (dom κ)) as (i & Hi).
+  exists i. intros k Hik Heq. subst κ.
+  specialize (Hi k). ospecialize (Hi _); last lia.
+  apply gmultiset_elem_of_dom.
+  apply gmultiset_elem_of_disj_union.
+  left. by apply gmultiset_elem_of_singleton.
+Qed.
 End creation.