proposition: Lemma composable_inverse : forall a u v, composable a u v -> invertible a u -> invertible a v -> composable a (inverse a v) (inverse a u).
proof: Proof. ir. cp (invertible_inverse H0). cp (invertible_inverse H1). cp H. rwi composable_facts_rw H; uh H; ee. ap show_composable. lu. lu. rw source_inverse; try am. rw target_inverse; try am. sy; am. Qed.
imports: Arith universe