proposition: Lemma lineatorinv_nat_right {ld : lineator_data} (ls : lineator_strongly ld) (lrn : lineator_nat_right ld) (v1 v2 : V) (x : C) (f : V⟦v1,v2⟧) : (is_z_isomorphism_mor (ls v1 x)) · f ⊗^{ActD}_{r} F x = #F (f ⊗^{ActC}_{r} x) · (is_z_isomorphism_mor (ls v2 x)).
proof: Proof. set (ldiso := ld v1 x ,, ls v1 x : z_iso _ _). apply (z_iso_inv_on_right _ _ _ ldiso). rewrite assoc. etrans. 2: { apply maponpaths_2. apply lrn. } rewrite assoc'. unfold is_z_isomorphism_mor. rewrite (pr12 (ls v2 x)). apply (! id_right _). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.coslicecat UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects