proposition: Lemma well_ordered_opposite r: worder r -> worder (opp_order r) -> finite_set (substrate r).
proof: Proof. move=> wor [ors wos]. move: (wor) => [or _]. set Z := Zo (substrate r) (fun x => (finite_set (segment r x))). have sZ1: sub Z (substrate r) by apply: Zo_S. move:(opp_osr or) => [pa pb]. have sZ: sub Z (substrate (opp_order r)) by rewrite pb. case: (emptyset_dichot (substrate r)) => sre. rewrite sre; apply: emptyset_finite. have neZ: nonempty Z. move: (worder_has_empty_seg wor sre) => [x xE sxe]. exists x; apply: Zo_i =>//. rewrite sxe; apply: emptyset_finite. move: (wos _ sZ neZ)=> [x []]; rewrite iorder_sr// =>xz. move:(xz) => /Zo_P [x1 x2] x3. set s:= segmentc r x. have fs: finite_set s by rewrite /s - (segmentc_pr or x1); apply: setU1_finite. case: (well_ordered_segment wor (segmentc_segment x or)); first by move <-. move=> [y ysr ss]. have yz: inc y Z by apply: Zo_i =>//; ue. move: (inc_bound_segmentc or x1); rewrite ss; move /segmentP => le1. move: (iorder_gle1 (x3 _ yz)) => /opp_gleP => yx; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)