some progress satisfying the obligations of diff

... in some of the most ugly proving ever. and with
still three dicey obligations to go.

which means that size.v doesn't yet compile
finished all of the running time related obligations for diff

still two obligations remaining (that corresponding to making sure we
satisfy the "P" argument in recursive calls)
diff obligations complete!
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
remove SearchAbout
got upper bound of sum_of_logs in the even case

Still have to do the odd case.
finish sum of logs odd
finish the odd case for the upper bound
I suppose this is really a Theorem, isn't it.
move make_array.v back out of old/

It was an accident I put it there. Sorry!
small cleanups
check lower bound
I feel like there should be an upper bound with a div2 in there
but I'm not sure what it is exactly

certainly the delta between the current upper bound and sum-of-logs
grows as n grows
use div2 instead of (proj1_sig (odd_S2n n' H)) or the even variant
minor size proof cleanup