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;