This gives the following new lemma:

```coq
Lemma mnat_auth_included q n : mnat_auth_frag n ≼ mnat_auth_auth q n.
```

Also reorganize the files slightly so that validity lemmas are grouped together.