proposition: 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: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics