Merge branch 'hai/frac_agree_included' into 'master'

Add included lemmas for frac_agree

See merge request iris/iris!665

iris/algebra/lib/frac_agree.v

@@ -48,6 +48,22 @@ Section lemmas.
     apply to_agree_op_invN. done.
   Qed.
 
+  Lemma frac_agree_included q1 a1 q2 a2 :
+    to_frac_agree q1 a1 ≼ to_frac_agree q2 a2 ↔
+    (q1 < q2)%Qp ∧ a1 ≡ a2.
+  Proof. by rewrite pair_included frac_included to_agree_included. Qed.
+  Lemma frac_agree_included_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
+    to_frac_agree q1 a1 ≼ to_frac_agree q2 a2 ↔
+    (q1 < q2)%Qp ∧ a1 = a2.
+  Proof. unfold_leibniz. apply frac_agree_included. Qed.
+  Lemma frac_agree_includedN q1 a1 q2 a2 n :
+    to_frac_agree q1 a1 ≼{n} to_frac_agree q2 a2 ↔
+    (q1 < q2)%Qp ∧ a1 ≡{n}≡ a2.
+  Proof.
+    by rewrite pair_includedN -cmra_discrete_included_iff
+               frac_included to_agree_includedN.
+  Qed.
+
   (** No frame-preserving update lemma needed -- use [cmra_update_exclusive] with
   the above [Exclusive] instance. *)