proposition: Lemma fusc_palindrome_bis u u' v w w' (aux := fun u v w => csucc(cdouble (\2c ^c v +c u)) *c (\2c ^c w)): natp u -> natp u' -> natp v -> natp w -> natp w' -> csucc (u +c u') = \2c ^c v -> fusc (aux u v w) = fusc (aux u' v w').
proof: Proof. move => uN u'N vN wN w'N eq. have Ha: forall u v w, natp u ->natp v -> natp w -> fusc (aux u v w) = Fusci (\2c ^c v +c u) \1c \1c. move => u1 v1 w1 u1n v1n w1n; rewrite /aux. move: (NS_sum (NS_pow NS2 v1n) u1n). set a := (\2c ^c v1 +c u1) => aN. move:(NS_succ (NS_double aN)); set b := (csucc (cdouble a)) => bN. rewrite - (fusci_val (NS_prod bN (NS_pow NS2 w1n))). transitivity (Fusci b \1c \0c); last first. rewrite fusci_odd ?(csum0r CS1); fprops. move:w1 w1n; apply: Nat_induction. by rewrite cpowx0 (cprod1r (CS_nat bN)). move => n nN <-; rewrite (cpow_succ _ nN) cprodA cprodC. by rewrite (fusci_even (NS_prod bN (NS_pow NS2 nN)) NS1 NS0) (csum0r CS1). rewrite (Ha _ _ _ uN vN wN) (Ha _ _ _ u'N vN w'N). exact: (fusci_palindrome_aux NS1 NS1 uN u'N vN eq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)