proposition: Lemma Exercise1_15a5 r A: sub A (substrate r) -> lo_bounds r (up_bounds r (lo_bounds r A)) = (lo_bounds r A).
proof: Proof. move=> Asr; apply: extensionality. apply: Exercise1_15a2; move=> t tA; move: (Asr _ tA) => tsr;apply: Zo_i =>//. by split => //; move=> y /Zo_hi [_]; apply. apply: Exercise1_15a4; apply: Zo_S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)