proposition: Lemma ringplusminus {R: ring} (a b : R) : (a + b - b)%ring = a.
proof: Proof. rewrite ringassoc1. rewrite ringrinvax1. apply (rigrunax1 R). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings