proposition: Lemma succ_inf_aux_p2: ((x +s1 a) \Eq (y +s1 b) -> x \Eq y).
proof: Proof. move =>[f [bf sf tf]]. move:(bf) =>[[ff injf] [_ sjf]]. have yt: inc b (target f) by rewrite tf; fprops. move: (inverse_V bf yt) (inverse_Vis bf yt). set a' := Vf (inverse_fun f) b => Wa asf'. exists (Lf (fun z => Yo (z = a') (Vf f a) (Vf f z)) x y); saw. have asf: inc a (source f) by rewrite sf; fprops. have sxsf: sub x (source f) by rewrite sf => t; fprops. apply: lf_bijective. + move=> z bx /=; Ytac ba. move: (Vf_target ff asf); rewrite tf. case /setU1_P => // h; rewrite - h in Wa; move: (injf _ _ asf' asf Wa). by move=> ab; case: nax; rewrite - ab - ba. have bsf: inc z (source f) by rewrite sf; fprops. move: (Vf_target ff bsf); rewrite tf. case /setU1_P => // h; rewrite -h in Wa; move: (injf _ _ asf' bsf Wa). by move=> ab; case: ba. + move=> u v ux vx; Ytac ua. Ytac va; first by rewrite ua va. move=> WW; move: (injf _ _ asf (sxsf _ vx) WW) => aux. by rewrite -aux in vx. Ytac va; last by move=> ww;apply: (injf _ _ (sxsf _ ux) (sxsf _ vx) ww). move=> WW;move: (injf _ _ (sxsf _ ux) asf WW) => aux. by case: nax; rewrite -aux. + move=> z zt. have ztf: (inc z (target f)) by rewrite tf; fprops. case: (equal_or_not z (Vf f a)) => zW. rewrite zW; exists a' => //; last by Ytac0. move: asf'; rewrite sf; case /setU1_P => //. by move=> ax;move: zt; rewrite zW; rewrite -{1} ax Wa. move: (sjf _ ztf) => [b' bsf Wb]. case: (equal_or_not b' a') => ba. by move: nby; rewrite - Wa - ba - Wb. exists b'; last by Ytac0. move: bsf; rewrite sf; case /setU1_P => // bx. by case: zW; rewrite Wb bx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)