let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of L st deg p > deg q holds
deg (p - q) = deg p
let p, q be Polynomial of L; :: thesis: ( deg p > deg q implies deg (p - q) = deg p )
assume A1: deg p > deg q ; :: thesis: deg (p - q) = deg p
A2: deg q = deg (- q) by POLYNOM4:8;
then deg (p + (- q)) = max ((deg p),(deg (- q))) by A1, HURWITZ:21;
hence deg (p - q) = deg p by A1, A2, XXREAL_0:def 10; :: thesis: verum