• Robbert Krebbers's avatar
    Rename `mnat`/`mnat_auth` into `mono_nat`. · 6b448546
    Robbert Krebbers authored
    - This avoids confusion between `mnat` and `max_nat`. The `m` stands for `mono`.
    - With `_mono` added, the `_auth` suffix in the algebra name no longer makes
      sense, so I removed it.
    - This makes the names between the logic and the algebra-level library consistent.
    - I also renamed `_frag` into `_lb` in the algebra-level library so as to make it
      consistent with the logic-level library.
    Furthermore make the order of lemmas consistent and make the versions for the
    fractions consistent.