proposition: Lemma STN_wosr: worder_on STN_order T1N.
proof: Proof. move: STN_osr => [ha hb]; split => //. case: (total_order_worder_dichot STN_tor) => // [] [f [fgf df rf fd]]. case:(not_decreasing nf_Wf). rewrite hb in rf. have hc: forall n, natp n -> inc (Vg f n) T1N. move => n nN; apply:rf; apply/(range_gP fgf); exists n => //; ue. pose g n := (set_to_T1 (Vg f (nat_to_B n))). exists g; move => i; rewrite /restrict. have sT: sub T1N T1 by apply:Zo_S. move: (nat_to_B_Nat i) (nat_to_B_Nat i.+1) => aN bN. have lt1: (nat_to_B i) <c (nat_to_B i.+1). by rewrite - nat_to_B_succ; apply:cltS. move:(hc _ aN) (hc _ bN) => hu hv. move:(hu)(hv)=> /Zo_P [aT1 Na] /Zo_P [bT1 Nb]; split => //. move:(fd _ _ aN bN lt1) => []. move/(iorder_gle0P _ hv hu) /ST1_leP => [_ _ sa] sb. rewrite T1lt_neAle /g sa andbT; apply/eqP => h; case sb. by apply:set_to_T1_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)