proposition: Lemma iorder_osr r a: order r -> sub a (substrate r) -> order_on (induced_order r a) a.
proof: Proof. move=> ar or. have: preorder (induced_order r a). by apply: iorder_preorder =>//; apply: order_preorder. move=> [go rio tio]; split. split => // x y /iorder_gleP [_ _ rxy] /iorder_gleP [_ _ ryz]; order_tac. set_extens t. by move/(substrate_P go) => [] [y] /iorder_gleP [pa pb _]. move => ta; move: (or _ ta) => tb. by apply /(substrate_P go); left; exists t; apply /iorder_gle0P => //;order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)