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 q
let p, q be Polynomial of L; :: thesis: ( deg p < deg q implies deg (p - q) = deg q )
assume A1: deg p < deg q ; :: thesis: deg (p - q) = deg q
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 q by A1, XXREAL_0:def 10; :: thesis: verum