proposition: Lemma posteq_rlmm_proper : forall i : I, θ' i = κ' i -> (θ' \O θ) i = (κ' \O θ) i.
proof: Proof. move=> i. cbv. move=> Heq. rewrite Heq. reflexivity. Qed.
imports: Coq(ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory)