proposition: Lemma Exercise1_20a r x: sub x (substrate r) -> scattered r -> scattered (induced_order r x).
proof: Proof. move=> xsr [or sc]; move: (iorder_osr or xsr) => [pa pb]. split => // y; rewrite pb => yx. by rewrite iorder_trans //; apply: sc; apply: (sub_trans yx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)