proposition: Lemma iorder_preorder r a: sub a (substrate r) -> preorder r -> preorder (induced_order r a).
proof: Proof. move=> ar [gr rr tr]. have gi: sgraph (induced_order r a) by apply: (setI2_graph1 gr (y:=coarse a)). hnf; split => //. move => t ti. have ta: inc t a. by move: ti => /(substrate_P gi) [] [y]/iorder_gleP [ta tb _]. by apply /iorder_gleP;split => //;apply: rr; apply: ar. move=> x y z /iorder_gleP [xa ya rxy] /iorder_gleP [_ za ryz]. apply/iorder_gleP;split => //; apply: tr rxy ryz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)