Theorem invOf_eq_left_inv

Modification history