proposition: Lemma setUf_segment r j s: (alls j (fun x => segmentp r (s x))) -> segmentp r (unionf j s).
proof: Proof. move=> als; split. move=> t tu;move: (setUf_hi tu)=> [y yj ts]. by move:(als _ yj) => [ss _]; apply: ss. move=> x y xu xy;move: (setUf_hi xu)=> [z zj ts]. move:(als _ zj) => [_ ss]; move: (ss _ _ ts xy) =>h; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)