proposition: Lemma issymmafldfracapartrelpre : issymm afldfracapartrelpre.
proof: Proof. intros ab cd. apply ( acommring_asymm A ). Defined.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields