proposition: 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: 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.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids