proposition: Lemma lassociator_to_rassociator_post {a b c d : C} {f : C ⟦ a, b ⟧} {g : C ⟦ b, c ⟧} {h : C ⟦ c, d ⟧} {k : C ⟦ a, d ⟧} (x : k ==> (f · g) · h) (y : k ==> f · (g · h)) (p : x = y • lassociator f g h) : x • rassociator f g h = y.
proof: Proof. use lhs_right_invert_cell. - apply is_invertible_2cell_rassociator. - exact p. Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct