proposition: Lemma inverse_comp : forall a u v, composable a u v -> invertible a u -> invertible a v -> inverse a (comp a u v) = comp a (inverse a v) (inverse a u).
proof: Proof. ir. ap inverse_eq. ap invertible_comp_are_inverse; am. Qed.
imports: Arith universe