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

got stuck trying to use Fix_eq.
more likely correct definitions of sum_of_logs_{even,odd}.

of course, this breaks size....
fix a bunch of stupid errors
change a lemma name to avoid shadowing stdlib name
started trying to show that sum_of_logs is related to log^2
proof for sum_of_logs_even