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