Lemma move_inv {C:category} {a a' b' b:C} {f : a --> b} {f' : a' --> b'} {i : a --> a'} {i' : a' --> a} {j : b --> b'} {j' : b' --> b} : is_inverse_in_precat i i' -> is_inverse_in_precat j j' -> j ∘ f = f' ∘ i -> j' ∘ f' = f ∘ i'. Proof. intros I J r. rewrite <- id_right. rewrite (! pr1 J). rewrite assoc. apply (maponpaths (λ k, j' ∘ k)). rewrite <- assoc. rewrite r. rewrite assoc. rewrite (pr2 I). rewrite id_left. reflexivity. Defined.
Require Import UniMath.MoreFoundations.Tactics.