proposition: Lemma fusc_normal_rec n: fusc (n.+2) + ((fusc n) %% fusc (n.+1)).*2 = (fusc n) + fusc (n.+1).
proof: Proof. elim/fusc_ind: n => //. move => n _; rewrite - doubleS ! fusc_even fusc_odd addnA addnn addnC. by rewrite modn_small // ltn_paddr // fusc_gt0. by move => n H _;rewrite - doubleS fusc_even !fusc_odd - addnA modnDr H addnC. 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)