proposition: Lemma fusci_palindrome_aux u u' v a b: natp a -> natp b -> natp u -> natp u' -> natp v -> csucc (u +c u') = \2c ^c v -> Fusci (\2c ^c v +c u) a b = Fusci (\2c ^c v +c u') b a.
proof: Proof. move => an bn un u'n vn; move: v vn u u' a b un u'n an bn. apply: Nat_induction. move => u u' a b uN u'N aN bN; rewrite cpowx0 - succ_zero. move /(csucc_inj (CS_sum2 u u') CS0) /csum_nz => [-> ->]. by rewrite succ_zero (csum0r CS1) (fusci_one aN bN) (fusci_one bN aN) csumC. move => n nN Hrec u u' a b uN u'N aN bN; rewrite - (cdouble_pow2 nN) => eq1. have p2N:=(NS_pow NS2 nN). case:(p_or_not_p (evenp (u +c u'))) => ouu. move:(succ_of_even ouu);rewrite eq1; move => [_]; case. apply:(even_double p2N). have: evenp u \/ evenp u'. case: (p_or_not_p (evenp u)) => ou; first by left. case: (p_or_not_p (evenp u')) => ou'; first by right. case: ouu; exact: (csum_of_odd (conj uN ou) (conj u'N ou')). wlog eu: a b aN bN u u' uN u'N eq1 ouu/ (evenp u). move => H ha;case: (ha) => aux; first by apply: H. by symmetry;apply: H => //; [rewrite csumC | rewrite csumC | left]. move:(NS_half uN) (NS_half u'N) => huN hu'N _. move: (NS_sum huN hu'N) => shN. move: (half_even eu) => h1. case: (cdouble_halfV u'N) => h2. by case: ouu; rewrite h1 h2 double_sum; apply: even_double;fprops. move: eq1; rewrite h1 h2 (csum_nS _ (NS_double hu'N)) double_sum. rewrite - (double_succ shN); move /(double_inj (NS_succ shN) p2N) => eq2. rewrite (csum_nS _ (NS_double hu'N)) ! double_sum. rewrite (fusci_even (NS_sum p2N huN) aN bN). rewrite (fusci_odd (NS_sum p2N hu'N) bN aN) (csumC b). exact: (Hrec _ _ _ _ huN hu'N (NS_sum aN bN) bN eq2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)