proposition: Lemma compare_wor_prop r r': worder r -> worder r' -> (r <=O r'<-> compare_wor r r').
proof: Proof. move => wo1 wo2; move: (proj1 wo1) (proj1 wo2) => or1 or2. split. move => [_ _ [f [x [sx fiso]]]]. case: (isomorphism_worder_sub wo2 sx). set w := iso_seg_fun _ _ => wa wb. have wc: (induced_order r' x) \Is (induced_order r' (target w)) by exists w. by split => //; exists (target w) => //; apply:orderIT wc; exists f. by move =>[_ _ [x [xs _] [f fi]]]; split => //; exists f,x. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)