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