rewrite > (H1 ? (hos_excess_ O)); lapply (hos_cotransitive O ?? z H);
[assumption] cases Hletin;[right|left]assumption;]
qed.
rewrite > (H1 ? (hos_excess_ O)); lapply (hos_cotransitive O ?? z H);
[assumption] cases Hletin;[right|left]assumption;]
qed.