Get rid of n_ary
Use to_real more often
Get rid of cantor_ary
Moving stuff around
Avoid some proofs by contradictions