2 is non trivial Nat by Def0;
hence a / (2 |^ (2 |-count a)) is integer ; :: thesis: verum