proposition: Lemma postLeq_rlmm_proper : forall i : I, θ' i ⪷ κ' i -> (θ' \O θ) i ⪷ (κ' \O θ) i.
proof: Proof. cbv. move=> i Hleq. apply Comp_proper. assumption. reflexivity. Qed.
imports: Coq(ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory)