theorem norm_one_sub_mul {R : Type u_1} [SeminormedRing R] {a b c : R} (ha : ‖a‖ ≤ 1) : ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖

theorem norm_one_sub_mul' {R : Type u_1} [SeminormedRing R] {a b c : R} (hb : ‖b‖ ≤ 1) : ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖

theorem nnnorm_one_sub_mul {R : Type u_1} [SeminormedRing R] {a b c : R} (ha : ‖a‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊

theorem nnnorm_one_sub_mul' {R : Type u_1} [SeminormedRing R] {a b c : R} (hb : ‖b‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖1 - a‖₊ + ‖c - b‖₊