proposition: Lemma worder_transportation r E G g: worder_on r E -> bijection_prop g E G -> exists2 s, worder_on s G & r \Is s.
proof: Proof. move =>[wor sr] [bg sf tg]. have sr1: (substrate r) = source g by ue. move:(order_transportation bg (conj (proj1 wor) sr1)); set s := Vfs _ _ => oig. have is1: r \Is s by exists g. move: (worder_invariance is1 wor) => wo1. exists s => //; split => //; rewrite - tg. by move: (oig) =>[_ _ [_ _ sr2] _]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)