proposition: Lemma Exercise4_7g a: inc a (substrate r) -> inc (the_least r) (E47S r a).
proof: Proof. move: Exercise4_7b=> or asr. move: (the_least_pr or (Exercise4_7c)) => [p1 p2]. apply: Zo_i => //;split;fprops. by move: Exercise4_7d => /Zo_P []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)