proposition: Lemma monotonic_bind : ((dnib W) f )∙1 w ≤ ((dnib W) f )∙1 w'.
proof: Proof. destruct (dnib W f) as [gg ggmon]. apply ggmon. assumption. Qed.
imports: Coq(Morphisms) mathcomp(all_ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples ChoiceAsOrd)