theorem
proved
periodicRelativeColumnOfRow5_encoded_endpoint_fst_eq_iff
show as:
periodicRelativeColumnOfRow5_encoded_endpoint_fst_eq_iff