proposition: Lemma T1graph_o: order_on T1graph T1.
proof: Proof. have ha: sgraph T1graph. by move => t /setI2_P [_ /setX_P []]. have rr: forall t, inc t T1 -> related T1graph t t. by move => t h; move:(T1graph_p1(T1lenn (Bo h))); rewrite B_eq. have hb: substrate T1graph = T1. set_extens t. by case/(substrate_P ha) => [] [y /T1graph_p2 []]; aw. move => /rr; apply:arg1_sr. have hc: reflexivep T1graph by move => t; rewrite hb; apply: rr. have hd: antisymmetricp T1graph. move => u v hu hv; move:(T1graph_p3 hu) (T1graph_p3 hv) => /=. set a := Bo _; set b := Bo _. set a' := Bo _; set b' := Bo _. have ea: u = Ro a by rewrite (B_eq (proj32 (T1graph_p2 hu))); aw. have eb: v = Ro b by rewrite (B_eq (proj33 (T1graph_p2 hu))); aw. have : v = Ro a' by rewrite (B_eq (proj32 (T1graph_p2 hv))); aw. have : u = Ro b' by rewrite (B_eq (proj33 (T1graph_p2 hv))); aw. rewrite ea eb => ec ed; rewrite - (R_inj ec) - (R_inj ed) => l1 l2. have -> // : a = b by apply/eqP; rewrite T1eq_le l1 l2. have he:transitivep T1graph. move => v u w hu hv. move:(T1graph_p3 hu) (T1graph_p3 hv) => /=. set a := Bo _; set b := Bo _; set c := Bo _; set d := Bo _. have ea: u = Ro a by rewrite (B_eq (proj32 (T1graph_p2 hu))); aw. have eb: v = Ro b by rewrite (B_eq (proj33 (T1graph_p2 hu))); aw. have: v = Ro c by rewrite (B_eq (proj32 (T1graph_p2 hv))); aw. have ed: w = Ro d by rewrite (B_eq (proj33 (T1graph_p2 hv))); aw. rewrite eb => ec; rewrite - (R_inj ec) => ab bd. by move:(T1graph_p1 (T1le_trans ab bd)); rewrite - ea - ed. by split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)