proposition: Lemma Exercise6_31_A z :inc z Z -> inc (rep z) F /\ gle r'' z (f (rep z)).
proof: Proof. move: Exercise6_31_i =>[or sr] /Exercise1_23aP [qa qb]. move: (rep_i qb) => yz. move: (proj1 (proj1 qa) _ yz) => ysr. move: (Exercise1_23d2 or ysr) => /Exercise1_23aP [p1 p2]. move: ysr; rewrite sr => yF; split => //. apply/(Exercise1_23bP or); split => //. rewrite /f /canonical_reg_open {2} (Exercise1_22p or qa). apply: (Exercise1_22j or (Exercise1_23c (rep z) or)(proj1 qa)). by move=> t /Zo_hi yt; move: (proj2 (proj1 qa) _ _ yz yt). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)