proposition: Proposition lr_rwhisker_v_comp_square {B : verity_double_bicat} {x₁ x₂ y₁ y₂ z₁ z₂ : B} {h₁ : x₁ --> x₂} {h₂ : y₁ --> y₂} {h₃ : z₁ --> z₂} {v₁ : x₁ -|-> y₁} {v₂ : y₁ -|-> z₁} {w₁ w₁' : x₂ -|-> y₂} {w₂ w₂' : y₂ -|-> z₂} (τ₁ : w₁ =|=> w₁') (τ₂ : w₂ =|=> w₂') (s₁ : square_double_bicat h₁ h₂ v₁ w₁) (s₂ : square_double_bicat h₂ h₃ v₂ w₂) : (τ₁ ▹s s₁) ⋆v (τ₂ ▹s s₂)= (τ₂ ⋆⋆ τ₁) ▹s s₁ ⋆v s₂.
proof: Proof. rewrite r_rwhisker_v_comp_square. rewrite l_rwhisker_v_comp_square. rewrite <- rwhisker_square_comp. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat