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