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