proposition: Lemma succ_inf_aux_p1: x \Eq y -> (x +s1 a) \Eq (y +s1 b).
proof: Proof. move=> [f [ [[ff injf] srjf] sf tf]]. have sjt: surjection (extension f a b) by apply: extension_fs =>//;ue. have st: source (extension f a b) = x +s1 a by rewrite /extension; aw;ue. have tt: target (extension f a b) = y +s1 b by rewrite /extension; aw;ue. have asf: ~ inc a (source f) by ue. exists (extension f a b); split => //. split => //; split; first by fct_tac. rewrite st; move=> u v; case /setU1_P=> us; case /setU1_P => vs. + rewrite ! extension_Vf_in //; try ue; apply: injf; ue. + rewrite (extension_Vf_in _ ff asf); last by ue. rewrite vs (extension_Vf_out _ ff asf);move =>h;case:nby;rewrite -h; Wtac. + rewrite us(extension_Vf_out _ ff asf)(extension_Vf_in _ ff asf);last by ue. move =>h; case: nby; rewrite h; Wtac. + rewrite us vs !extension_Vf_out //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)