:: Schur's Theorem on the Stability of Networks
:: by Agnieszka Rowi\'nska-Schwarzweller and Christoph Schwarzweller
::
:: Received October 19, 2006
:: Copyright (c) 2006 Association of Mizar Users

Lm1: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of L
for G being FinSequence
for k being Nat st G = F | (Seg k) & len F = k + 1 holds
( G is FinSequence of L & dom G c= dom F & len G = k & F = G ^ <*(F /. (k + 1))*> )

proof end;

theorem Th1: :: HURWITZ:1

for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for x being Element of L st x <> 0. L holds
- (x " ) = (- x) "

proof end;

theorem Th2: :: HURWITZ:2

for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for k being Element of NAT holds (power L) . (- (1_ L)),k <> 0. L

proof end;

theorem Th3: :: HURWITZ:3

for L being non empty associative well-unital multLoopStr
for x being Element of L
for k1, k2 being Element of NAT holds ((power L) . x,k1) * ((power L) . x,k2) = (power L) . x,(k1 + k2)

proof end;

Lm2: ( Im (1_ F_Complex ) = 0 & Im (- (1_ F_Complex )) = 0 & Im (0. F_Complex ) = 0 )

proof end;

Lm3: for z being Element of F_Complex st Im z = 0 holds
z *' = z

proof end;

theorem Th4: :: HURWITZ:4

for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for k being Element of NAT holds
( (power L) . (- (1_ L)),(2 * k) = 1_ L & (power L) . (- (1_ L)),((2 * k) + 1) = - (1_ L) )

proof end;

theorem Th5: :: HURWITZ:5

for z being Element of F_Complex
for k being Element of NAT holds ((power F_Complex ) . z,k) *' = (power F_Complex ) . (z *' ),k

proof end;

theorem Th6: :: HURWITZ:6

for F, G being FinSequence of F_Complex st len G = len F & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) holds
Sum G = (Sum F) *'

proof end;

theorem Th7: :: HURWITZ:7

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for F1, F2 being FinSequence of L st len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds
F1 /. i = - (F2 /. i) ) holds
Sum F1 = - (Sum F2)

proof end;

theorem Th8: :: HURWITZ:8

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for x being Element of L
for F being FinSequence of L holds x * (Sum F) = Sum (x * F)

proof end;

Lm4: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds - (- p) = p

proof end;

theorem Th9: :: HURWITZ:9

for L being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0_. L) = 0_. L

proof end;

Lm5: for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for f being Element of (Polynom-Ring L) st f = p holds
- f = - p

proof end;

theorem :: HURWITZ:10

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds - (- p) = p by Lm4;

theorem Th11: :: HURWITZ:11

for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L holds - (p1 + p2) = (- p1) + (- p2)

proof end;

theorem Th12: :: HURWITZ:12

for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L holds
( - (p1 *' p2) = (- p1) *' p2 & - (p1 *' p2) = p1 *' (- p2) )

proof end;

definition

let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let F be FinSequence of (Polynom-Ring L);
let i be Element of NAT ;
func Coeff F,i -> FinSequence of L means :Def1: :: HURWITZ:def 1
( len it = len F & ( for j being Element of NAT st j in dom it holds
ex p being Polynomial of L st
( p = F . j & it . j = p . i ) ) );
existence
ex b₁ being FinSequence of L st
( len b₁ = len F & ( for j being Element of NAT st j in dom b₁ holds
ex p being Polynomial of L st
( p = F . j & b₁ . j = p . i ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of L st len b₁ = len F & ( for j being Element of NAT st j in dom b₁ holds
ex p being Polynomial of L st
( p = F . j & b₁ . j = p . i ) ) & len b₂ = len F & ( for j being Element of NAT st j in dom b₂ holds
ex p being Polynomial of L st
( p = F . j & b₂ . j = p . i ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Coeff HURWITZ:def 1 :

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for F being FinSequence of (Polynom-Ring L)
for i being Element of NAT
for b₄ being FinSequence of L holds
( b₄ = Coeff F,i iff ( len b₄ = len F & ( for j being Element of NAT st j in dom b₄ holds
ex p being Polynomial of L st
( p = F . j & b₄ . j = p . i ) ) ) );

theorem Th13: :: HURWITZ:13

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for F being FinSequence of (Polynom-Ring L) st p = Sum F holds
for i being Element of NAT holds p . i = Sum (Coeff F,i)

proof end;

Lm6: for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L
for p2' being Element of (Polynom-Ring L) st p2' = p2 holds
for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p2' * F)

proof end;

theorem Th14: :: HURWITZ:14

for L being non empty associative doubleLoopStr
for p being Polynomial of L
for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) * p

proof end;

theorem Th15: :: HURWITZ:15

for L being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for x being Element of L holds - (x * p) = (- x) * p

proof end;

theorem Th16: :: HURWITZ:16

for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for x being Element of L holds - (x * p) = x * (- p)

proof end;

theorem Th17: :: HURWITZ:17

for L being non empty left-distributive doubleLoopStr
for p being Polynomial of L
for x1, x2 being Element of L holds (x1 + x2) * p = (x1 * p) + (x2 * p)

proof end;

theorem Th18: :: HURWITZ:18

for L being non empty right-distributive doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L holds x * (p1 + p2) = (x * p1) + (x * p2)

proof end;

theorem Th19: :: HURWITZ:19

for L being non empty right_complementable associative commutative distributive add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)

proof end;

definition

let L be non empty ZeroStr ;
let p be Polynomial of L;
func degree p -> Integer equals :: HURWITZ:def 2
(len p) - 1;
coherence
(len p) - 1 is Integer ;

end;

:: deftheorem defines degree HURWITZ:def 2 :

for L being non empty ZeroStr
for p being Polynomial of L holds degree p = (len p) - 1;

notation

let L be non empty ZeroStr ;
let p be Polynomial of L;
synonym deg p for degree p;

end;

Lm7: for L being non empty ZeroStr
for s being AlgSequence of L st len s > 0 holds
s . ((len s) - 1) <> 0. L

proof end;

theorem Th20: :: HURWITZ:20

for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p = - 1 iff p = 0_. L )

proof end;

Lm8: for L being non empty ZeroStr
for p being Polynomial of L st deg p <> - 1 holds
p . (deg p) <> 0. L

proof end;

Lm9: for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )

proof end;

theorem :: HURWITZ:21

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p1, p2 being Polynomial of L st deg p1 <> deg p2 holds
deg (p1 + p2) = max (deg p1),(deg p2)

proof end;

Lm10: for L being non empty ZeroStr
for p being Polynomial of L holds deg p >= - 1

proof end;

theorem Th22: :: HURWITZ:22

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p1, p2 being Polynomial of L holds deg (p1 + p2) <= max (deg p1),(deg p2)

proof end;

theorem Th23: :: HURWITZ:23

for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p1, p2 being Polynomial of L st p1 <> 0_. L & p2 <> 0_. L holds
deg (p1 *' p2) = (deg p1) + (deg p2)

proof end;

theorem Th24: :: HURWITZ:24

for L being non empty right_complementable unital add-associative right_zeroed doubleLoopStr
for p being Polynomial of L st deg p = 0 holds
not p is with_roots

proof end;

Lm11: for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT st k <> 0 holds
( ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . 0 = - ((power L) . z,k) & ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . k = 1_ L )

proof end;

Lm12: for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT
for i being Nat st i <> 0 & i <> k holds
((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . i = 0. L

proof end;

definition

let L be non empty unital doubleLoopStr ;
let z be Element of L;
let k be Element of NAT ;
func rpoly k,z -> Polynomial of L equals :: HURWITZ:def 3
(0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L));
coherence
(0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L)) is Polynomial of L

proof end;

end;

:: deftheorem defines rpoly HURWITZ:def 3 :

for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT holds rpoly k,z = (0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L));

theorem :: HURWITZ:25

for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT st k <> 0 holds
( (rpoly k,z) . 0 = - ((power L) . z,k) & (rpoly k,z) . k = 1_ L ) by Lm11;

theorem :: HURWITZ:26

for L being non empty unital doubleLoopStr
for z being Element of L
for i, k being Element of NAT st i <> 0 & i <> k holds
(rpoly k,z) . i = 0. L by Lm12;

theorem Th27: :: HURWITZ:27

for L being non empty non degenerated well-unital doubleLoopStr
for z being Element of L
for k being Element of NAT holds deg (rpoly k,z) = k

proof end;

theorem Th28: :: HURWITZ:28

for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L holds
( deg p = 1 iff ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly 1,z) ) )

proof end;

theorem Th29: :: HURWITZ:29

for L being non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr
for x, z being Element of L holds eval (rpoly 1,z),x = x - z

proof end;

theorem Th30: :: HURWITZ:30

for L being non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr
for z being Element of L holds z is_a_root_of rpoly 1,z

proof end;

definition

let L be non empty well-unital doubleLoopStr ;
let z be Element of L;
let k be Nat;
func qpoly k,z -> Polynomial of L means :Def4: :: HURWITZ:def 4
( ( for i being Nat st i < k holds
it . i = (power L) . z,((k - i) - 1) ) & ( for i being Nat st i >= k holds
it . i = 0. L ) );
existence
ex b₁ being Polynomial of L st
( ( for i being Nat st i < k holds
b₁ . i = (power L) . z,((k - i) - 1) ) & ( for i being Nat st i >= k holds
b₁ . i = 0. L ) )

proof end;

uniqueness
for b₁, b₂ being Polynomial of L st ( for i being Nat st i < k holds
b₁ . i = (power L) . z,((k - i) - 1) ) & ( for i being Nat st i >= k holds
b₁ . i = 0. L ) & ( for i being Nat st i < k holds
b₂ . i = (power L) . z,((k - i) - 1) ) & ( for i being Nat st i >= k holds
b₂ . i = 0. L ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines qpoly HURWITZ:def 4 :

for L being non empty well-unital doubleLoopStr
for z being Element of L
for k being Nat
for b₄ being Polynomial of L holds
( b₄ = qpoly k,z iff ( ( for i being Nat st i < k holds
b₄ . i = (power L) . z,((k - i) - 1) ) & ( for i being Nat st i >= k holds
b₄ . i = 0. L ) ) );

theorem :: HURWITZ:31

for L being non empty non degenerated well-unital doubleLoopStr
for z being Element of L
for k being Element of NAT st k >= 1 holds
deg (qpoly k,z) = k - 1

proof end;

theorem Th32: :: HURWITZ:32

for L being non empty right_complementable commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr
for z being Element of L
for k being Element of NAT st k > 1 holds
(rpoly 1,z) *' (qpoly k,z) = rpoly k,z

proof end;

theorem Th33: :: HURWITZ:33

for L being non empty right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for z being Element of L st z is_a_root_of p holds
ex s being Polynomial of L st p = (rpoly 1,z) *' s

proof end;

definition

let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let p, s be Polynomial of L;
assume A1: s <> 0_. L ;
func p div s -> Polynomial of L means :Def5: :: HURWITZ:def 5
ex t being Polynomial of L st
( p = (it *' s) + t & deg t < deg s );
existence
ex b₁, t being Polynomial of L st
( p = (b₁ *' s) + t & deg t < deg s )

proof end;

uniqueness
for b₁, b₂ being Polynomial of L st ex t being Polynomial of L st
( p = (b₁ *' s) + t & deg t < deg s ) & ex t being Polynomial of L st
( p = (b₂ *' s) + t & deg t < deg s ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines div HURWITZ:def 5 :

for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, s being Polynomial of L st s <> 0_. L holds
for b₄ being Polynomial of L holds
( b₄ = p div s iff ex t being Polynomial of L st
( p = (b₄ *' s) + t & deg t < deg s ) );

definition

let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let p, s be Polynomial of L;
func p mod s -> Polynomial of L equals :: HURWITZ:def 6
p - ((p div s) *' s);
coherence
p - ((p div s) *' s) is Polynomial of L ;

end;

:: deftheorem defines mod HURWITZ:def 6 :

for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, s being Polynomial of L holds p mod s = p - ((p div s) *' s);

definition

let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let p, s be Polynomial of L;
pred s divides p means :Def7: :: HURWITZ:def 7
p mod s = 0_. L;

end;

:: deftheorem Def7 defines divides HURWITZ:def 7 :

for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, s being Polynomial of L holds
( s divides p iff p mod s = 0_. L );

theorem Th34: :: HURWITZ:34

for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, s being Polynomial of L st s <> 0_. L holds
( s divides p iff ex t being Polynomial of L st t *' s = p )

proof end;

theorem :: HURWITZ:35

for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for z being Element of L st z is_a_root_of p holds
rpoly 1,z divides p

proof end;

theorem :: HURWITZ:36

for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for z being Element of L st p <> 0_. L & z is_a_root_of p holds
deg (p div (rpoly 1,z)) = (deg p) - 1

proof end;

definition

let f be Polynomial of F_Complex ;
attr f is Hurwitz means :Def8: :: HURWITZ:def 8
for z being Element of F_Complex st z is_a_root_of f holds
Re z < 0 ;

end;

:: deftheorem Def8 defines Hurwitz HURWITZ:def 8 :

for f being Polynomial of F_Complex holds
( f is Hurwitz iff for z being Element of F_Complex st z is_a_root_of f holds
Re z < 0 );

theorem :: HURWITZ:37

not 0_. F_Complex is Hurwitz

proof end;

theorem :: HURWITZ:38

for x being Element of F_Complex st x <> 0. F_Complex holds
x * (1_. F_Complex ) is Hurwitz

proof end;

theorem Th39: :: HURWITZ:39

for x, z being Element of F_Complex st x <> 0. F_Complex holds
( x * (rpoly 1,z) is Hurwitz iff Re z < 0 )

proof end;

theorem Th40: :: HURWITZ:40

for f being Polynomial of F_Complex
for z being Element of F_Complex st z <> 0. F_Complex holds
( f is Hurwitz iff z * f is Hurwitz )

proof end;

Lm13: for f, g, h being Polynomial of F_Complex st f = g *' h holds
for x being Element of F_Complex st ( x is_a_root_of g or x is_a_root_of h ) holds
x is_a_root_of f

proof end;

theorem Th41: :: HURWITZ:41

for f, g being Polynomial of F_Complex holds
( f *' g is Hurwitz iff ( f is Hurwitz & g is Hurwitz ) )

proof end;

definition

let f be Polynomial of F_Complex ;
func f *' -> Polynomial of F_Complex means :Def9: :: HURWITZ:def 9
for i being Element of NAT holds it . i = ((power F_Complex ) . (- (1_ F_Complex )),i) * ((f . i) *' );
existence
ex b₁ being Polynomial of F_Complex st
for i being Element of NAT holds b₁ . i = ((power F_Complex ) . (- (1_ F_Complex )),i) * ((f . i) *' )

proof end;

uniqueness
for b₁, b₂ being Polynomial of F_Complex st ( for i being Element of NAT holds b₁ . i = ((power F_Complex ) . (- (1_ F_Complex )),i) * ((f . i) *' ) ) & ( for i being Element of NAT holds b₂ . i = ((power F_Complex ) . (- (1_ F_Complex )),i) * ((f . i) *' ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines *' HURWITZ:def 9 :

for f, b₂ being Polynomial of F_Complex holds
( b₂ = f *' iff for i being Element of NAT holds b₂ . i = ((power F_Complex ) . (- (1_ F_Complex )),i) * ((f . i) *' ) );

theorem Th42: :: HURWITZ:42

for f being Polynomial of F_Complex holds deg (f *' ) = deg f

proof end;

theorem Th43: :: HURWITZ:43

for f being Polynomial of F_Complex holds (f *' ) *' = f

proof end;

theorem Th44: :: HURWITZ:44

for f being Polynomial of F_Complex
for z being Element of F_Complex holds (z * f) *' = (z *' ) * (f *' )

proof end;

theorem Th45: :: HURWITZ:45

for f being Polynomial of F_Complex holds (- f) *' = - (f *' )

proof end;

theorem Th46: :: HURWITZ:46

for f, g being Polynomial of F_Complex holds (f + g) *' = (f *' ) + (g *' )

proof end;

theorem Th47: :: HURWITZ:47

for f, g being Polynomial of F_Complex holds (f *' g) *' = (f *' ) *' (g *' )

proof end;

Lm14: for x, xv being Element of COMPLEX
for u, v, uv, vv being Element of REAL st x = u + (v * <i> ) & xv = uv + (vv * <i> ) holds
(|.(x + (xv *' )).| ^2 ) - (|.(x - xv).| ^2 ) = (4 * u) * uv

proof end;

Lm15: for x, xv being Element of COMPLEX
for u, v, uv, vv being Element of REAL st x = u + (v * <i> ) & xv = uv + (vv * <i> ) & uv < 0 holds
( ( u < 0 implies |.(x - xv).| < |.(x + (xv *' )).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *' )).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *' )).| ) )

proof end;

theorem Th48: :: HURWITZ:48

for x, z being Element of F_Complex holds eval ((rpoly 1,z) *' ),x = (- x) - (z *' )

proof end;

theorem Th49: :: HURWITZ:49

for f being Polynomial of F_Complex st f is Hurwitz holds
for x being Element of F_Complex st Re x >= 0 holds
0 < |.(eval f,x).|

proof end;

theorem Th50: :: HURWITZ:50

for f being Polynomial of F_Complex st deg f >= 1 & f is Hurwitz holds
for x being Element of F_Complex holds
( ( Re x < 0 implies |.(eval f,x).| < |.(eval (f *' ),x).| ) & ( Re x > 0 implies |.(eval f,x).| > |.(eval (f *' ),x).| ) & ( Re x = 0 implies |.(eval f,x).| = |.(eval (f *' ),x).| ) )

proof end;

definition

let f be Polynomial of F_Complex ;
let z be Element of F_Complex ;
func F* f,z -> Polynomial of F_Complex equals :: HURWITZ:def 10
((eval (f *' ),z) * f) - ((eval f,z) * (f *' ));
coherence
((eval (f *' ),z) * f) - ((eval f,z) * (f *' )) is Polynomial of F_Complex ;

end;

:: deftheorem defines F* HURWITZ:def 10 :

for f being Polynomial of F_Complex
for z being Element of F_Complex holds F* f,z = ((eval (f *' ),z) * f) - ((eval f,z) * (f *' ));

theorem Th51: :: HURWITZ:51

for a, b being Element of F_Complex st |.a.| > |.b.| holds
for f being Polynomial of F_Complex st deg f >= 1 holds
( f is Hurwitz iff (a * f) - (b * (f *' )) is Hurwitz )

proof end;

theorem Th52: :: HURWITZ:52

for f being Polynomial of F_Complex st deg f >= 1 holds
for rho being Element of F_Complex st Re rho < 0 & f is Hurwitz holds
(F* f,rho) div (rpoly 1,rho) is Hurwitz

proof end;

theorem :: HURWITZ:53

for f being Polynomial of F_Complex st deg f >= 1 & ex rho being Element of F_Complex st
( Re rho < 0 & |.(eval f,rho).| >= |.(eval (f *' ),rho).| ) holds
not f is Hurwitz by Th50;

theorem :: HURWITZ:54

for f being Polynomial of F_Complex st deg f >= 1 holds
for rho being Element of F_Complex st Re rho < 0 & |.(eval f,rho).| < |.(eval (f *' ),rho).| holds
( f is Hurwitz iff (F* f,rho) div (rpoly 1,rho) is Hurwitz )

proof end;