proposition: Lemma Exercise1_15a18a x: inc x (substrate r) -> inc x (lobs x).
proof: Proof. by move=> xsr; apply: Zo_i => //; split => //;move=> u /set1_P ->; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)