New lemma data_at_conflict_glb

[andrew-appel]

New lemma data_at_conflict_glb. See also: https://stackoverflow.com/questions/77305287/why-does-data-at-conflict-require-identical-shares/

[roconnor-blockstream]

FWIW I wrote also wrote the following lemmas today:

Lemma nonempty_writable0_glb (shw shr : share) : writable0_share shw -> readable_share shr ->
  nonempty_share (Share.glb shw shr).
Proof.
intros Hshw Hshr.
apply leq_join_sub in Hshw.
apply Share.ord_spec2 in Hshw.
rewrite Share.glb_commute, <- Hshw, Share.distrib1, Share.glb_commute, Share.lub_commute.
apply readable_nonidentity.
apply readable_share_lub.
apply readable_glb.
assumption.
Qed.

Lemma nonempty_writable_glb (shw shr : share) : writable_share shw -> readable_share shr ->
  nonempty_share (Share.glb shw shr).
Proof.
intros Hshw Hshr.
apply nonempty_writable0_glb; try assumption.
apply writable_writable0; assumption.
Qed.

Though I'm sure someone with more familiarity can write more concise proofs of these.