+lemma l2sl_:
+ ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
+intros; intro; apply H; apply sx2x_; apply H1;
+qed.
+
+
+lemma sl2l_:
+ ∀C,s.∀x,y:half_segment_ordered_set C s. x ≤≤ y → \fst x ≤≤ \fst y.
+intros; intro; apply H; apply x2sx_; apply H1;
+qed.
+
+coercion x2sx_ nocomposites.
+coercion sx2x_ nocomposites.
+coercion l2sl_ nocomposites.
+coercion sl2l_ nocomposites.
+