proposition: Lemma fusc2_surjective a b: natp a -> natp b -> b <> \0c -> BZcoprime (BZ_of_nat a) (BZ_of_nat b) -> exists n, [/\ natp n, fusc n = a & fusc (csucc n) = b].
proof: Proof. move => na nb. move: fusc_pr => [Ha Hb Hc Hd]. move:(NS_sum na nb) => h; move:(cleR (CS_nat h)); move: h. move: {1 3} (a +c b) => n nN; move: n nN a b na nb; apply:Nat_induction. move => a b aN bN /cle0 /csum_nz [az bz] _. rewrite az bz /BZcoprime (BZgcd_zero ZS0) BZabs_0 => /pr1_def h. by case: card1_nz. move => n nN Hrec a b aN bN lea bnz gcd. move:(BZ_of_nat_i aN)(BZ_of_nat_i bN) => az bz. case: (NleT_ell bN aN) => le1. + move: gcd; rewrite le1 /BZcoprime (BZgcd_id az) => h. move: (f_equal P h); rewrite BZabs_val /BZ_one /BZ_of_nat; aw => a1. by exists \1c;rewrite succ_one fusc2 Hb; split; fprops. + have sa:=(cdiff_pr (proj1 le1)). have baN:=(NS_diff b aN). have le2: (a -c b) +c b <=c n. rewrite csumC sa; apply/(cltSleP nN). apply:(clt_leT (csum_M0lt aN bnz) lea). have gcd1 :BZcoprime (BZ_of_nat (a -c b)) (BZ_of_nat b). move:(f_equal BZ_of_nat sa); rewrite - (BZsum_cN bN baN) => /esym. move/(BZsum_diff_ea bz (BZ_of_nat_i baN)) => ->; apply: BZcoprime_sym. by apply:BZcoprime_diff => //; apply:BZcoprime_sym . move: (Hrec _ _ baN bN le2 bnz gcd1) => [k [kN e1 e2]]. exists (csucc (cdouble k)); rewrite (Hd _ kN) - (double_succ kN). rewrite (Hc _ (NS_succ kN)) e1 e2 csumC sa; split => //. apply: (NS_succ (NS_double kN)). + have sa := (cdiff_pr (proj1 le1)). case: (equal_or_not a \0c) => anz. move:gcd; rewrite anz /BZcoprime BZgcd_C (BZgcd_zero bz)=> h. move: (f_equal P h); rewrite BZabs_val /BZ_one /BZ_of_nat; aw => a1. exists \0c; rewrite succ_zero Ha Hb a1; split => //; apply:NS0. have b'nz:=(cdiff_nz le1). have baN:=(NS_diff a bN). have le2: a +c (b -c a) <=c n. rewrite sa; apply/(cltSleP nN); apply:(clt_leT _ lea). by rewrite csumC; apply:csum_M0lt. have gcd1 :BZcoprime (BZ_of_nat a) (BZ_of_nat (b -c a)). move:(f_equal BZ_of_nat sa); rewrite - (BZsum_cN aN baN) => /esym. by move/(BZsum_diff_ea az (BZ_of_nat_i baN)) => ->; apply: BZcoprime_diff. move: (Hrec _ _ aN baN le2 b'nz gcd1) => [k [kN e1 e2]]. exists (cdouble k); rewrite (Hc _ kN) (Hd _ kN) e1 e2 sa; split => //. exact (NS_double kN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)