proposition: Lemma normR_max a b c c' : 0 <= a <= c -> 0 <= b <= c' -> `| a - b | <= max(c, c').
proof: Proof. move=> [H1 H2] [H H3]; case: (Rtotal_order a b) => [H0|[H0|H0]]. - rewrite distRC gtR0_norm ?subR_gt0 //. apply: (@leR_trans b); [Lra.lra | apply/(leR_trans H3)/leR_maxr; lra]. - subst b; rewrite subRR normR0. exact/(leR_trans H1)/(leR_trans H2)/leR_maxl. - rewrite geR0_norm; last Lra.lra. apply: (@leR_trans a); [Lra.lra|exact/(leR_trans H2)/leR_maxl]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)