Lemma triple_ref_greater_abstract : forall (p:loc) (n:int), triple (ref_greater p) (p ~~> n) (funloc q => \exists m, \[m > n] \* q ~~> m \* p ~~> n). Proof using. intros. xapp triple_ref_greater. xsimpl. { auto. } { math. } Qed.