proposition: Lemma inverse_unique : forall a u v w, are_inverse a u v -> are_inverse a u w -> v = w.
proof: Proof. ir. uh H; uh H0; ee. transitivity (comp a (comp a v u) w). rw assoc. rw H4. rw right_id. tv. uh H0; ee. cw. am. rww H3. tv. am. am. am. am. am. tv. rw H10. cw. cw. sy; am. Qed.
imports: Arith universe