proposition: Lemma normD x y : norm (x + y) <= norm x + norm y.
proof: Proof. rewrite /norm num_le_maxl !(le_trans (ler_normD _ _)) ?lerD//; by rewrite comparable_le_maxr ?lexx ?orbT// real_comparable. Qed.
imports: HB(structures) mathcomp(all_ssreflect fingroup ssralg poly ssrnum) signed