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