proposition: Lemma invertible_comp_are_inverse : forall a u v, composable a u v -> invertible a u -> invertible a v -> are_inverse a (comp a u v) (comp 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. uhg; ee; try am. cw. lu. lu. cw. sy; lu. cw. lu. lu. cw. sy; lu. cw. lu. lu. cw. sy; lu. cw. rw assoc. assert (comp a v (comp a (inverse a v) (inverse a u))= inverse a u). wr assoc. cw. cw. cw. cw. cw. cw. lu. cw. cw. sy; lu. tv. rw H12. cw. lu. lu. cw. lu. lu. cw. sy; lu. lu. cw. lu. lu. cw. sy; lu. tv. lu. lu. cw. sy; lu. rw assoc. assert (comp a (inverse a u) (comp a u v) = v). wrr assoc. cw. cw. sy; lu. cw. cw. rw H12. cw. cw. cw. cw. cw. sy; lu. cw. tv. Qed.
imports: Arith universe