proposition: Lemma applied_ord_relmon_law1 : forall (A : I) x, dnib M (η M A) x = x.
proof: Proof. move=> A. move=> x. rewrite ord_relmon_law1. simpl. reflexivity. Qed.
imports: Coq(Morphisms) mathcomp(all_ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples ChoiceAsOrd)