proposition: Lemma spec_applied_ord_relmon_law3 : forall (A B C : I) (f : OrdCat ⦅ J B; M C ⦆) (g : OrdCat ⦅ J A; M B ⦆) x, (dnib M (dnib M f ∙ g))∙1 x = (dnib M f)∙1 ( (dnib M g)∙1 x).
proof: Proof. move=> A B C f g x. simpl. epose (aux := (ord_relmon_law3 M) A B C f g). apply (f_equal sval) in aux. simpl in aux. 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)