proposition: Lemma ltz0_abs m : (m < 0)%R -> `|m| = - m :> int.
proof: Proof. by case: (intP m). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)