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