proposition: Lemma isomorphism_worder_exists_v1 r r' (f := iso_seg_fun r r'): worder r -> worder r' -> iso_seg_iso r r' f \/ iso_seg_iso r' r (inverse_fun f).
proof: Proof. move => wo1 wo2. move:(proj1 wo1) (proj1 wo2) => o1 o2. move:(iso_graph_prop wo1 wo2) => /=. move => [ha hb hc hd]; case: hc => hc; [left | right]. by move: hd; rewrite hc (iorder_substrate o1) => hd. move: hd; rewrite hc (iorder_substrate o2) => hd. by saw; apply: inverse_order_is. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)