Useful lemma for users: nonempty_writable_glb

[andrew-appel]

Perhaps add these lemmas to Floyd (see #732 (comment) )

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.