Definition isinvbinophrellogeqf {X : setwithbinop} {L R : hrel X} (lg : hrellogeq L R) (isl : isinvbinophrel L) : isinvbinophrel R. Proof. split. - intros a b c rab. apply ((pr1 (lg _ _) ((pr1 isl) _ _ _ (pr2 (lg _ _) rab)))). - intros a b c rab. apply ((pr1 (lg _ _) ((pr2 isl) _ _ _ (pr2 (lg _ _) rab)))). Defined.