+lemma hint_segment: ∀O.
+ segment (Type_of_ordered_set O) →
+ segment (hos_carr (os_l O)).
+intros; assumption;
+qed.
+
+coercion hint_segment nocomposites.
+
+lemma segment_square_of_ordered_set_square:
+ ∀O:ordered_set.∀s:‡O.∀x:O squareO.
+ \fst x ∈ s → \snd x ∈ s → {[s]} squareO.
+intros; split; exists; [1: apply (\fst x) |3: apply (\snd x)] assumption;
+qed.
+
+coercion segment_square_of_ordered_set_square with 0 2 nocomposites.
+
+alias symbol "pi1" (instance 4) = "exT \fst".
+alias symbol "pi1" (instance 2) = "exT \fst".
+lemma ordered_set_square_of_segment_square :
+ ∀O:ordered_set.∀s:‡O.{[s]} squareO → O squareO ≝
+ λO:ordered_set.λs:‡O.λb:{[s]} squareO.〈\fst(\fst b),\fst(\snd b)〉.
+
+coercion ordered_set_square_of_segment_square nocomposites.