More consistent naming for `auth`.

This MR is a follow up on the renamings performed (implicitly) as part of !215 (merged). This MR makes the following changes:

• auth_both_frac_valid and auth_both_valid are now of the same shape as auth_both_frac_validN and auth_both_validN. That is, both are now biimplications.
• The left-to-right direction of auth_both_frac_valid and auth_both_valid only holds in case the camera is discrete. The right-to-left versions for non-discrete cameras are suffixed _2, the convention that we use throughout the development.
• Change the direction of lemmas like auth_frag_valid and auth_auth_valid so that it's consistent with the other lemmas. I.e. make sure that the ◯ and ● are always on the LHS of the biimplication.