got size going, except for two "obvious" lemmas
about sum_of_logs

got stuck trying to use Fix_eq.