proposition: Lemma ler_dist_dist v w : `| `|v| - `|w| | <= `|v - w|.
proof: Proof. have [||_|_] // := @real_leP `|v| `|w|; last by rewrite lerB_dist. by rewrite distrC lerB_dist. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)