Lemma isinvrigmultgtif (X : commrig) (R : hrel X) (is2 : ∏ a b c d, R (op1 (op2 a c) (op2 b d)) (op1 (op2 a d) (op2 b c)) → R a b → R c d) : isinvrigmultgt X R. Proof. intros. split. - apply is2. - intros a b c d r rcd. rewrite (rigcomm1 X (op2 a d) _) in r. rewrite (rigcomm2 X a c) in r. rewrite (rigcomm2 X b d) in r. rewrite (rigcomm2 X b c) in r. rewrite (rigcomm2 X a d) in r. apply (is2 _ _ _ _ r rcd). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.