Make validy lemmas for `excl_auth` and `(u)frac_auth` more consistent with `auth`.

• Make validy lemmas for excl_auth more consistent with auth.
  • Rename excl_auth_frag_validN_op_1_l into excl_auth_frag_op_validN and excl_auth_frag_valid_op_1_l into excl_auth_frag_op_valid (similar to auth_auth_op_valid), and make them bi-implications.
  • Add excl_auth_auth_op_validN and excl_auth_auth_op_valid.
• Make validy lemmas for (u)frac_auth more consistent with auth.
  • Remove unidirectional lemmas with 1 fraction frac_auth_frag_validN_op_1_l and frac_auth_frag_valid_op_1_l
  • Add frac_auth_frag_op_validN and frac_auth_frag_op_valid, which are bi-implications with arbitrary fractions.
  • Add ufrac_auth_frag_op_validN and ufrac_auth_frag_op_valid.

I think the old names were a consequence of porting lemmas like:

Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯F{1} a ⋅ ◯F{q} b) → False.