per cases ( p <> 0_. L or p = 0_. L ) ;

suppose p <> 0_. L ; :: thesis: ( ( p <> 0_. L implies deg p is Nat ) & ( not p <> 0_. L implies 0 is Nat ) )

then not p is zero by UPROOTS:def 5;
hence ( ( p <> 0_. L implies deg p is Nat ) & ( not p <> 0_. L implies 0 is Nat ) ) by TARSKI:1; :: thesis: verum

end;

suppose p = 0_. L ; :: thesis: ( ( p <> 0_. L implies deg p is Nat ) & ( not p <> 0_. L implies 0 is Nat ) )

hence ( ( p <> 0_. L implies deg p is Nat ) & ( not p <> 0_. L implies 0 is Nat ) ) ; :: thesis: verum

end;

end;