proposition: Lemma fusc_prevE n (P:= fun x y => x * ((y %/x).+1 - (y%%x==0).*2) - y%% x): fusc n = P (fusc n.+1)(fusc n.+2).
proof: Proof. move:(fusc_normal_rec n); rewrite /P. set A := fusc n; set B := fusc _ ; set C := fusc _. move: (divn_eq A C); set q := A %/ C; set r := A %% C => eq /eqP. have cp: 0 < C by rewrite fusc_gt0. have rC: r < C by rewrite ltn_mod. have cv:= (subnK (ltnW rC)). rewrite {1} eq addnAC -{2} cv -!addnA addnn addnA eqn_add2r => /eqP eq2. case eq1 :(r == 0). move: eq eq2; rewrite (eqP eq1) addn0 subn0 - mulSnr => -> ->. by rewrite mulnK // modnMl mulnC subn2 !succnK subn0. have hn: C -r < C by rewrite -{2}cv - {1}[C-r]addn0 ltn_add2l lt0n eq1. move: (edivn_eq q hn); rewrite - eq2 edivn_def mulnC eqn0Ngt; case => -> ->. by rewrite subn_gt0 rC subn0 mulSnr - addnBA ?(ltnW hn) // subKn // (ltnW rC). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)