proposition: Lemma iso_unique_bis r r' f f': worder r' -> order_isomorphism f r r' -> order_isomorphism f' r r' -> f = f'.
proof: Proof. move => wor ha hb. have iso: r' \Is r by exists (inverse_fun f); apply:(inverse_order_is ha). exact: (iso_unique (worder_invariance iso wor) ha hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)