proposition: Lemma ipreorder_sr r a: preorder r -> sub a (substrate r) -> substrate (induced_order r a) = a.
proof: Proof. move => ha hb. have /substrate_P sp: sgraph (induced_order r a). by move => t /setI2_P [_]/setX_P[]. set_extens t. by move/sp => [] [y] /iorder_gleP [pa pb _]. move => ta; move: (hb _ ta) => tb. apply /sp; left; exists t; apply /iorder_gle0P => //. by apply: (proj32 ha). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)