proposition: Lemma fusc_rec: fusc_prop fusc.
proof: Proof. set F := fix loop n k := if k is k'.+1 then if n<=1 then n else if (odd n) then (loop n./2 k') + loop (uphalf n) k' else loop n./2 k' else 0. pose G n k := if n<=1 then n else if (odd n) then (F n./2 k) + F (uphalf n) k else F n./2 k. have Hc: forall n k, F n k = if k is k'.+1 then G n k' else 0 by move => a []. have aux: forall n m, n <= m -> F n n = F n m. move => n m le; move: {1 3 5 }n (leqnn n). move => p; move: p n le; elim:m; first by move => p []. move =>m IHm p [ _ | n]; first by case p. rewrite Hc Hc /G ltnS => lenm lepn. have [// | le_p_n ] := leqP p 1. have ha: p./2 <= n by move:(leq_trans (half_le3w le_p_n) lepn); rewrite ltnS. rewrite (IHm _ _ lenm ha); case op: (odd p) => //;rewrite (IHm _ _ lenm) //. rewrite (oddE op) /= doubleK ltn_neqAle ha andbT; apply/negP; move/eqP => eq2. move: lepn le_p_n; rewrite (oddE op) eq2 ltnS - {2} (doubleK n) => /half_le4. by case n. split => //. case=> // n; rewrite {+} /fusc -/F. by rewrite doubleS Hc /G ltnS ltn0 - doubleS odd_double doubleK - (aux _ _ (double_le2 n)). case => // n; rewrite {+} /fusc -/F. rewrite -/(F n.+1 n.+1) -/(F n.+2 n.+2) -/(F (n.+1).*2.+1 (n.+1).*2.+1 ). rewrite Hc /G /odd -/odd odd_double [_ ./2 ] (uphalf_double n.+1). rewrite [(uphalf (n.+1).*2.+1) ] (doubleK (n.+2)). by rewrite (aux _ _ ( double_le3 n)) (aux _ _ (leqW (double_le2 n))). 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)