let R be non degenerated Ring; :: thesis: for p being non zero Polynomial of R holds deg (p - (LM p)) < deg p
let p be non zero Polynomial of R; :: thesis: deg (p - (LM p)) < deg p

per cases ( p - (LM p) = 0_. R or p - (LM p) <> 0_. R ) ;

suppose p - (LM p) = 0_. R ; :: thesis: deg (p - (LM p)) < deg p

hence deg (p - (LM p)) < deg p by HURWITZ:20; :: thesis: verum

end;

suppose p - (LM p) <> 0_. R ; :: thesis: deg (p - (LM p)) < deg p

then reconsider q = p - (LM p) as non zero Polynomial of R by UPROOTS:def 5;

A: now :: thesis: not deg q = deg p

assume deg q = deg p ; :: thesis: contradiction
then LC q = q . (deg p) by thLC
.= (p . (deg p)) - ((LM p) . (deg p)) by POLYNOM3:27
.= (p . (deg p)) - ((LM p) . (deg (LM p))) by thdegLM
.= (p . (deg p)) - (LC (LM p)) by thLC
.= (p . (deg p)) - (LC p) by thdegLC
.= (LC p) - (LC p) by thLC
.= 0. R by RLVECT_1:15 ;
hence contradiction ; :: thesis: verum

end;

now :: thesis: not deg q > deg p

assume B0: deg q > deg p ; :: thesis: contradiction
then deg q >= (deg p) + 1 by INT_1:7;
then B1: deg q >= ((len p) - 1) + 1 by HURWITZ:def 2;
p <> 0_. R ;
then len p <> 0 by POLYNOM4:5;
then (len p) + 1 > 0 + 1 by XREAL_1:6;
then D: len p >= 1 by NAT_1:13;
deg q <> (len p) - 1 by B0, HURWITZ:def 2;
then deg q <> (len p) -' 1 by D, XREAL_0:def 2;
then B2: (LM p) . (deg q) = 0. R by POLYNOM4:def 1;
LC q = q . (deg q) by thLC
.= (p . (deg q)) - ((LM p) . (deg q)) by POLYNOM3:27
.= (0. R) - (0. R) by ALGSEQ_1:8, B1, B2 ;
hence contradiction ; :: thesis: verum

end;

hence deg (p - (LM p)) < deg p by A, XXREAL_0:1; :: thesis: verum

end;

end;