This MR is a follow up on the renamings performed (implicitly) as part of !215 (merged). This MR makes the following changes:
auth_both_validare now of the same shape as
auth_both_validN. That is, both are now biimplications.
- The left-to-right direction of
auth_both_validonly 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_auth_validso that it's consistent with the other lemmas. I.e. make sure that the ◯ and ● are always on the LHS of the biimplication.