Lemma iscompbinoptransrel {X : setwithbinop} (R : hrel X) (ist : istrans R) (isb : isbinophrel R) : iscomprelrelfun2 R R (@op X). Proof. intros a b c d. intros rab rcd. set (racbc := pr2 isb a b c rab). set (rbcbd := pr1 isb c d b rcd). apply (ist _ _ _ racbc rbcbd). Defined.