proposition: Lemma STN_tor: total_order STN_order.
proof: Proof. move: STN_osr => [ha hb]; split => //; rewrite hb => x y xE yE. have s1: sub T1N T1 by apply: Zo_S. move:(s1 _ xE)(s1 _ yE) => x1 y1. case /orP: (T1le_total(set_to_T1 x)(set_to_T1 y)) => h. + left; apply/iorder_gle0P => //; apply/ ST1_leP; split => //. + right; apply/iorder_gle0P => //; apply/ ST1_leP; split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)