proposition: Lemma mulr_absz (x : R) i : x *+ `|i| = x *~ `|i|.
proof: Proof. by rewrite -abszE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)