proposition: Lemma fusc_col_progression i j: natp i -> natp j -> j <=c \2c ^c i -> fusc(\2c ^c (csucc i) +c j) = fusc(\2c ^c i +c j) +c fusc j.
proof: Proof. move: fusc_pr => [Ha Hb Hc Hd]. move => iN; move: i iN j; apply: Nat_induction. move => j jN; rewrite succ_zero cpowx0 (cpowx1 CS2). move/(cltSleP NS1); rewrite succ_one => /clt2; case => ->. by rewrite (csum0r CS2)(csum0r CS1) fusc2 Ha Hb (csum0r CS1). by rewrite - (Nsucc_rw NS2) - (cprod1r CS2) (Hd _ NS1) csumC (Nsucc_rw NS1). move => n nN Hrec j jN le1. have hjN:=(NS_half jN). have snN:=(NS_succ nN). move: le1; rewrite -(cdouble_pow2 nN) - (cdouble_pow2 snN). case: (cdouble_halfV jN) => eq1; rewrite eq1 => le1. have na: natp (\2c ^c csucc n +c chalf j) by fprops. have nb: natp (\2c ^c n +c chalf j) by fprops. rewrite (Hc _ hjN) double_sum double_sum {1} (Hc _ na) (Hc _ nb). apply: (Hrec _ hjN (cprod_le2l NS2 hjN (NS_pow NS2 nN) card2_nz le1)). have ha:=(NS_double hjN). have hb:natp (\2c ^c csucc n +c chalf j) by fprops. have hc: natp (\2c ^c n +c chalf j) by fprops. rewrite !(csum_nS _ ha) !double_sum. rewrite {1} (Hd _ hb) (Hd _ hc) (Hd _ hjN) - ! (csum_nS _ hjN). have lt1:csucc (chalf j) <=c \2c ^c n. apply /(cleSltP hjN); move/(cleSltP ha): le1. apply:(cprod_lt2l NS2 hjN (NS_pow NS2 nN)). have lt2:chalf j <=c \2c ^c n by move:(cleT (cleS hjN) lt1). rewrite (Hrec _ hjN lt2) (Hrec _ (NS_succ hjN) lt1);rewrite - 2! csumA. by apply: f_equal; rewrite csumA csumA (csumC (fusc (chalf j))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)