proposition: Lemma image_of_inf r r' f: worder r -> worder r' -> order_isomorphism f r r' -> nonempty (substrate r) -> (inc (the_least r) (source f) /\ Vf f (the_least r) = the_least r').
proof: Proof. move=> wor wor' [o1 o2 [bf sf tf] oif] ne1. have ne2: nonempty (substrate r'). move: ne1 => [x xs]; exists (Vf f x); rewrite - tf. apply: Vf_target; [fct_tac | ue]. move: (the_least_pr o1 (worder_least wor ne1)). move: (the_least_pr o2 (worder_least wor' ne2)). set x := the_least r; set y := the_least r'; move => pc [pa pb]. split ; [ by ue | apply: (unique_least o2) => // ]. rewrite - sf in pa. split; first by Wtac; fct_tac. rewrite - tf => z zt; move: bf => [_ sjf]. move: ((proj2 sjf) _ zt) => [t tsf ->]; rewrite - oif //. apply: pb; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)