proposition: Lemma Exercise1_15a1 r A B: sub A B -> sub (up_bounds r B) (up_bounds r A).
proof: Proof. move => AB t /Zo_P [tsr [_ p2]]; apply /Zo_i => //. by split=> //; move=> y yA; apply: p2; apply: AB. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)