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