proposition: Lemma Exercise6_31_l z: inc z Z -> exists2 x, inc x Ex6_31_res & gle r'' z (f x).
proof: Proof. move => zZ; move: (proj2 (Exercise6_31_A zZ)) => h. exists (rep z) => //. apply/Ex6_31_resP. move:(Exercise6_31_k zZ) =>[<- _ _ _ _]; exists z, \0c; split => //; apply: NS0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)