proposition: Lemma are_inverse_transfo_inverse : forall u v : E, are_inverse u v -> Transformation.are_inverse (U (source u)) (U (target u)) ( ev u) (ev v).
proof: Proof. ir. unfold Transformation.are_inverse in |- *. unfold are_inverse in H. xe. unfold composable in H; xe. unfold composable in H, H0; xe. rewrite <- H4. rewrite H6. am. ir. transitivity (ev (compose v u) x). sy; ap ev_compose. am. rewrite H2. ap ev_identity. am. ir. assert (inc y (U (source v))). unfold composable in H0; xe. rewrite H5; am. transitivity (ev (compose u v) y). rewrite ev_compose. tv. am. rewrite H1. rewrite ev_identity. tv. am. Qed.
imports: Arith functions