Lemma natmult_binophrel {X : monoid} (R : hrel X) : istrans R → isbinophrel R → ∏ (n : nat) (x y : X), R x y → R (natmult (S n) x) (natmult (S n) y). Proof. intros Hr Hop n x y H. induction n as [|n IHn]. exact H. rewrite !(natmultS (S _)). eapply Hr. apply (pr1 Hop). exact IHn. apply (pr2 Hop). exact H. Qed.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.DivisionRig. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.ConstructiveStructures. Require Import UniMath.MoreFoundations.Tactics.