proposition: Lemma fuscj_reverse n: natp n -> Fuscj n \0c = Fuscj \0c (base_two_reverse n).
proof: Proof. move:(cprod0r \2c) n => d2. pose R a b := (b *c \2c ^c (clog2 a) +c (base_two_reverse a)). suff: forall a, natp a -> forall b, natp b -> Fuscj a b = Fuscj \0c (R a b). by move => H n nN; rewrite(H _ nN _ NS0) /R cprod0l (Nsum0l (NS_reverse nN)). have aux: forall b, natp b -> Fuscj \0c b = Fuscj \0c (R \0c b). move => b bN. by rewrite /R clog0 base2r_zero cpowx0 (cprod1r (CS_nat bN))(Nsum0r bN). apply: fusc_induction. + by move => b bN; apply: aux. + move => b bN; rewrite /R base2r_one clog1 (cpowx1 CS2) cprodC (fuscj_one bN). by rewrite (Nsucc_rw (NS_double bN)). + move => k kN Ha b bN. case: (equal_or_not k \0c) => knz. by rewrite knz cdouble0; apply: aux. rewrite /R (clog_double kN knz) (base2r_even kN) - (cdouble_pow2 (NS_log kN)). by rewrite(fuscj_even kN bN) (Ha _ (NS_double bN)) /R cprodA (cprodC b). + move => k kN Ha Hb b bN. rewrite (fuscj_odd kN bN) (Ha _ (NS_succ (NS_double bN))) /R (base2r_odd kN). rewrite csumA (clog_succ_double kN) - (cdouble_pow2 (NS_log kN)) cprodA. by rewrite cprodC (cprod_nS _ (NS_double bN)) cprodC (cprodC b). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)