proposition: Lemma applied_ord_relmon_law3 : forall (A B C : I) (f : TypeCat ⦅ J B; M C ⦆) (g : TypeCat ⦅ J A; M B ⦆) x, dnib M (dnib M f ∙ g) x = dnib M f ( dnib M g x).
proof: Proof. move=> A B C f g x. epose (aux := (ord_relmon_law3 M) A B C f g). unshelve eapply equal_f in aux. exact x. assumption. Qed.
imports: Coq(Morphisms) mathcomp(all_ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples ChoiceAsOrd)