proposition: Lemma Ex6_31_resP t: inc t Ex6_31_res <-> exists z n, [/\ inc z Z, inc n Nat & t = Ex6_31_Xnz z n].
proof: Proof. split; [ by move/Zo_hi | move => h; move: (h) =>[z [n [zZ nN ->]]]]. move:(Exercise6_31_k zZ) =>[_ hh _ _ _]. by apply: (Zo_i (hh _ nN)); exists z,n. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)