lapply (segment_preserves_supremum s a ≪?,h≫ H2) as Ha2;
cases Ha2; clear Ha2;
cases (H1 a a); lapply (H5 H3 Ha1) as HaC;
lapply (segment_cauchy C s ? HaC) as Ha;
lapply (sigma_cauchy ? H ? x ? Ha); [left; assumption]
lapply (segment_preserves_supremum s a ≪?,h≫ H2) as Ha2;
cases Ha2; clear Ha2;
cases (H1 a a); lapply (H5 H3 Ha1) as HaC;
lapply (segment_cauchy C s ? HaC) as Ha;
lapply (sigma_cauchy ? H ? x ? Ha); [left; assumption]