proposition: Lemma hqldistr : ∏ x y z, x * (y + z) = x * y + x * z.
proof: Proof. intros x y z. now apply ringldistr. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.NumberSystems.RationalNumbers UniMath.Algebra.Archimedean