Lemma isbinophrelif {X : setwithbinop} (R : hrel X) (is : iscomm (@op X)) (isl : ∏ a b c : X, R a b → R (op c a) (op c b)) : isbinophrel R. Proof. exists isl. intros a b c rab. induction (is c a). induction (is c b). apply (isl _ _ _ rab). Defined.