proposition: Lemma lerB_dist v w : `|v| - `|w| <= `|v - w|.
proof: Proof. by rewrite -[`|w|]normrN lerB_normD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)