proposition: Lemma fusc_palindrome n a b (p := \2c ^c n): natp n -> p <=c a -> a <=c cdouble p -> p <=c b -> b <=c cdouble p -> a +c b = \3c *c p -> fusc a = fusc b.
proof: Proof. move: fusc_pr => [Ha Hb Hc Hd]. rewrite /p; clear p;move => nN; move: n nN a b; apply: Nat_induction. move => a b; rewrite cpowx0 /cdouble (cprod1r CS2) (cprod1r (CS_nat NS3)). move => ha hb hc hd he. have ->: fusc a = \1c. case: (equal_or_not a \2c) => ca2; first by rewrite ca2 fusc2. case/clt2: (conj hb ca2); last by move => ->. by move => az; case: card1_nz; apply:cle0; rewrite - az. have -> //: fusc b = \1c. case: (equal_or_not b \2c) => cb2; first by rewrite cb2 fusc2. case/clt2: (conj hd cb2); last by move => ->. by move => bz; case: card1_nz; apply:cle0; rewrite - bz. move => n nN Hrec a b. rewrite -(cdouble_pow2 nN); set p := (\2c ^c n); rewrite -/p in Hrec. rewrite -/(cdouble _) => pa pb pc pd pe. have pN: natp p by apply:(NS_pow NS2 nN). have p2N := (NS_double pN). have p4N :=(NS_double p2N). have aN:= (NS_le_nat pb p4N). have bN:= (NS_le_nat pd p4N). move: (NS_half aN)(NS_half bN) => haN hbN. rewrite double_prod in pe. case: (cdouble_halfV aN) => ea. case: (cdouble_halfV bN) => eb. rewrite ea eb; rewrite (Hc _ haN) (Hc _ hbN); apply: Hrec. + by apply/(double_monotone pN haN); rewrite - ea. + by apply/(double_monotone haN p2N); rewrite - ea. + by apply/(double_monotone pN hbN); rewrite - eb. + by apply/(double_monotone hbN p2N); rewrite - eb. move: pe; rewrite {1} ea {1} eb double_sum. apply/(double_inj (NS_sum haN hbN) (NS_prod NS3 pN)). have ha: natp (cdouble (chalf b)) by apply: NS_double. move:pe; rewrite {1} ea {1} eb (csum_nS _ ha) double_sum => h. move:(even_double (NS_sum haN hbN)) (even_double(NS_prod NS3 pN)) => sa sb. by move: (succ_of_even sa); rewrite h; case => [_]. case: (cdouble_halfV bN) => eb. have ha: natp (cdouble (chalf a)) by apply: NS_double. move:pe; rewrite {1} ea {1} eb (csum_Sn _ ha) double_sum => h. move:(even_double (NS_sum haN hbN)) (even_double(NS_prod NS3 pN)) => sa sb. by move:(succ_of_even sa); rewrite h; case => [_]. rewrite ea eb (Hd _ haN) (Hd _ hbN). rewrite ea in pa pb. rewrite eb in pc pd. have h1:=(double_le_odd1 haN pN pa). have h2:=(double_le_odd1 hbN pN pc). have h3:=(double_le_odd2 haN p2N pb). have h4:=(double_le_odd2 hbN p2N pd). have bN': natp (csucc (cdouble (chalf b))) by ue. have aN':= (NS_double haN). have e1: chalf a +c csucc (chalf b) = \3c *c p. apply:( double_inj (NS_sum haN (NS_succ hbN)) (NS_prod NS3 pN)). rewrite - double_sum (double_succ hbN) (csum_nS _ bN') - eb. by rewrite - (csum_Sn _ aN') - ea pe. rewrite - (Hrec _ _ h1 (cleT (cleS haN) h3) (cleT h2 (cleS hbN)) h4 e1). move: e1; rewrite (csum_nS _ hbN) - (csum_Sn _ haN) => e1. by rewrite(Hrec _ _ (cleT h1 (cleS haN)) h3 h2 (cleT (cleS hbN) h4) e1) csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)