proposition: Lemma ispartinvbinophrelif {X : setwithbinop} (S : hsubtype X) (R : hrel X) (is : iscomm (@op X)) (isl : ∏ a b c : X, S c -> R (op c a) (op c b) -> R a b) : ispartinvbinophrel S R.
proof: Proof. split with isl. intros a b c s rab. destruct (is c a). destruct (is c b). apply (isl _ _ _ s rab). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions