proposition: Lemma Exercise2_6a: inc (substrate r) bigS.
proof: Proof. apply: Zo_i; aw; first by apply /setP_P; fprops. split. move => x xsr; move: (fxx xsr) => h; order_tac. by move=> N x Nsr [y yN] /(lubP or Nsr) [[p1 _] _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)