proposition: Lemma ST1_osr: order_on ST1_order T1.
proof: Proof. have rr: forall a, inc a T1 -> (ST1_le a a) by move => h; split => //. move: (graph_on_sr rr); rewrite -/ ST1_order => st; split => //. apply:order_from_rel; split. + move => y x t [xE yE ha] [_ zE /(T1le_trans ha) hb]; split => //. + move => x y [xE yE ha][_ _ hb]. by apply:set_to_T1_inj=> //; apply/eqP; rewrite T1eq_le ha hb. + by move => u v [uE vE _]; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)