reconsider m = n as Divisor of n by Def2;
take m ; :: thesis: not m is trivial
thus not m is trivial ; :: thesis: verum