use div2 instead of (proj1_sig (odd_S2n n' H)) or the even variant
minor size proof cleanup