proposition: Lemma inverse_unique : forall u v w : E, strong_axioms v -> strong_axioms w -> are_inverse u v -> are_inverse u w -> v = w.
proof: Proof. ir. transitivity (compose v (identity (source v))). sy. ap right_identity. am. unfold are_inverse in H1, H2; ee. assert (source v = target u). unfold composable in H6; xe. assert (source v = source w). rewrite H9. unfold composable in H3; xe. rewrite H10. rewrite <- H4. rewrite <- associativity. rewrite H8. assert (source u = target w). unfold composable in H2; xe. rewrite H11. ap left_identity. am. am. am. Qed.
imports: Arith functions