proposition: Lemma sub_inf_aux: sub x y -> x \Eq (x +s1 a) -> y \Eq (y +s1 b).
proof: Proof. move=> sxy /EqS [f [[[ff injf] sjf] sf tf]]. have nbx: ~ inc b x by dneg bx; apply: sxy. apply:EqS. have Asf: inc a (source f) by rewrite sf; fprops. have wafx: inc (Vf f a) x by Wtac. set g := fun z => Yo (inc z x) (Vf f z) (Yo (z = b) (Vf f a) z). have Byp: forall t, inc t y -> t <> b by move=> t ty tB; case: nby; ue. have pa: lf_axiom g (y +s1 b) y. move=> t /setU1_P; rewrite /g; case. move=> ty; Ytac tx; first by apply: sxy; Wtac; rewrite sf; fprops. by move: (Byp _ ty) => aux; Ytac0. by move => ->; Ytac0; Ytac0; apply: sxy. have pb: forall u v, inc u (y +s1 b) -> inc v (y +s1 b) -> g u = g v -> u = v. move=> u v; rewrite /g; case /setU1_P => uy /setU1_P aux; last first. rewrite uy; Ytac0; Ytac0; Ytac vx. have vsf: inc v (source f) by rewrite sf; fprops. by move=> h; rewrite -(injf _ _ Asf vsf h) in vx. case:aux => vy //. by move: (Byp _ vy) => aux;Ytac0 => h; rewrite -h in vx. Ytac ux. Ytac vx; first by apply: injf; rewrite sf; fprops. case: aux => vy. move: (Byp _ vy) => aux; Ytac0=> h; case: vx; rewrite -h -tf. Wtac; rewrite sf; fprops. Ytac0 => aux. have usf: inc u (source f) by rewrite sf; fprops. by rewrite (injf _ _ usf Asf aux) in ux. have uB: u <> b by move => ub; case: nby; ue. Ytac0; Ytac vx. move=> h; rewrite h in ux; case: ux; rewrite -tf. Wtac; rewrite sf; fprops. case: aux => vy; [move: (Byp _ vy) => aux |]; Ytac0 => //. move=> h;case: ux; ue. exists (Lf g (y +s1 b) y); saw; apply: lf_bijective => // t ty. case: (inc_or_not t x) => tx. rewrite -tf in tx; move: ((proj2 sjf) _ tx)=> [z zsf wz]. move: zsf; rewrite sf;case /setU1_P => zx. exists z; first by apply /setU1_P; left; apply: sxy. by rewrite /g; Ytac0. by exists b; fprops; rewrite /g; Ytac0; Ytac0; rewrite - zx wz. by move: (Byp _ ty) => aux;exists t; fprops;rewrite /g; Ytac0; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)