Add `and_own` lemma for handling `own γ x ∧ own γ y`

The main purpose is to add the following result:

  Lemma and_own (γ : gname) (x y : A) :
    (own γ x ∧ own γ y) ⊢ ∃ z , own γ z 
        ∗ Some x ≼ Some z
        ∗ Some y ≼ Some z.

The reason we use Some x ≼ Some z is because we need the comparison to be reflexive.

Here, the ≼ is defined to be an iProp version of the normal ≼:

Definition uPred_cmra_included {Σ: gFunctors} {M: cmra} (a b : M) : iProp Σ := ∃ c , b ≡ a ⋅ c.
Infix "≼" := uPred_cmra_included (at level 70) : bi_scope.

We also prove some corollaries of and_own, e.g., for a discrete unital camera we have:

  Lemma and_own_discrete_ucmra_specific {D : CmraDiscrete A} (γ : gname) (x y z : A) :
    (∀ w , ✓ w → x ≼ w → y ≼ w → z ≼ w) →
    (own γ x ∧ own γ y) ⊢ own γ z.

  Lemma and_own_discrete_ucmra_contradiction {D : CmraDiscrete A} (γ : gname) (x y : A) :
    (∀ w , ✓ w → x ≼ w → y ≼ w → False) →
    (own γ x ∧ own γ y) ⊢ False.

All the new code is in own.v; I think the new ≼ should probably go somewhere else but I wasn't quite sure where.