( not 2 is trivial & a <> 0 & not 2 divides a ) ;
hence 2 |-count a is zero by NAT327; :: thesis: verum