Lemma ringminusdistl { X : commring } ( a b c : X ) : (b - c) * a = b * a - c * a. Proof. intros. rewrite ringrdistr. rewrite ringlmultminus. apply idpath. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.