proposition: Lemma Exercise1_21aP r v: order r -> sub v (substrate r) -> (scattered (induced_order r v) <-> (forall u, sub u v -> ~ without_gaps (induced_order r u))).
proof: Proof. move => or vsr; rewrite /scattered. move: (iorder_osr or vsr) => [pa pb];rewrite pb => //; split. by move=> [oi h] u uv; move: (h _ uv); rewrite iorder_trans. move=> h;split;fprops;move=> x xv; move:(h _ xv); rewrite iorder_trans //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)