proposition: 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: Proof. split with isl. intros a b c rab. destruct (is c a). destruct (is c b). apply (isl _ _ _ rab). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions