explain why gmap_view_both_dfrac_valid_discrete_total is unidirectional

iris/algebra/lib/gmap_view.v

@@ -307,6 +307,11 @@ Section lemmas.
       split; first by apply cmra_valid_validN.
       by apply: cmra_included_includedN.
   Qed.
+  (** The backwards direction here does not hold: if [dq = DfracOwn 1] but
+  [v ≠ v'], we have to find a suitable erased fraction [dq'] to satisfy the view
+  relation, but there is no way to satisfy [Some (DfracOwn 1, v) ≼ Some (dq', v')]
+  for any [dq']. The "if and only if" version of this lemma would have to
+  involve some extra condition like [dq = DfracOwn 1 → v = v'].  *)
   Lemma gmap_view_both_dfrac_valid_discrete_total
       `{!CmraDiscrete V, !CmraTotal V} dp m k dq v :
     ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) →