add lemams for validity of the 1 fraction

iris/algebra/dfrac.v

@@ -160,6 +160,8 @@ Section dfrac.
 
   Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
+  Lemma dfrac_valid_own_1 : ✓ DfracOwn 1.
+  Proof. done. Qed.
 
   Lemma dfrac_valid_own_r dq q : ✓ (dq ⋅ DfracOwn q) → (q < 1)%Qp.
   Proof.

iris/algebra/frac.v

@@ -21,6 +21,8 @@ Section frac.
 
   Lemma frac_valid p : ✓ p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
+  Lemma frac_valid_1 : ✓ 1%Qp.
+  Proof. done. Qed.
   Lemma frac_op p q : p ⋅ q = (p + q)%Qp.
   Proof. done. Qed.
   Lemma frac_included p q : p ≼ q ↔ (p < q)%Qp.