proposition: Lemma Exercise1_15a6 r A: sub A (substrate r) -> uplo_bounds r (uplo_bounds r A) = (uplo_bounds r A).
proof: Proof. move=> Asr; rewrite /uplo_bounds Exercise1_15a5 /up_bounds//. apply: Zo_S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)