proposition: Fact le_normD x y : `|x + y| <= `|x| + `|y|.
proof: Proof. wlog x_ge0 : x y / 0 <= x. by move=> IH; case: (leN_total x) => /IH// /(_ (- y)); rewrite -opprD !normN. rewrite -sub_ge0 ge0_norm //; have [y_ge0 | ny_ge0] := leN_total y. by rewrite !ge0_norm ?subrr ?le0_add. rewrite -normN ge0_norm //; have [hxy|hxy] := leN_total (x + y). by rewrite ge0_norm // opprD addrCA -addrA addKr le0_add. by rewrite -normN ge0_norm // opprK addrCA addrNK le0_add. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)