proposition: Lemma fusc_rec_spec1 n i (q := \2c ^c n)(p := cdouble q) : natp n -> i <=c q -> fsimpl_sum p i = BQdiv (BQ_of_nat (fusc i)) (BQ_of_nat (fusc (p +c i))).
proof: Proof. move => nN lin; rewrite /fsimpl_sum. have qN: natp q by exact:(NS_pow NS2 nN). have pN: natp p by exact:(NS_double qN). have iN:=(NS_le_nat lin qN). move: i iN lin; apply: Nat_induction. move => _; rewrite qsum0 fusc0 BQdiv_0x //; apply: QS_of_nat. exact:(NS_fusc (NS_sum pN NS0)). move => i iN Hrec lt1. have piN := (NS_sum pN iN). rewrite (qsum_rec _ iN) (Hrec (cleT (cleS iN) lt1)). move/(cleSltP iN): lt1 => lt1. move: (NS_fusc piN) (NS_fusc (NS_sum pN (NS_succ iN))). set a := fusc _; set b := fusc _ => aN bN. move: (QS_of_nat aN)(QS_of_nat bN);set a' := BQ_of_nat a; set b' :=BQ_of_nat b. move: (NS_fusc iN) => siN; move:(QS_of_nat siN) => cq aq bq. move: (NS_fusc (NS_succ iN)) => kiN; move:(QS_of_nat kiN) => kiq. have anz: a' <> \0q. move/(BQ_of_nat_injective); apply: (fusc_nz (NS_sum pN iN)) => /csum_nz. by move: (double_nz qN (@cpow2_nz n)) => [ha _] []. have bnz: b' <> \0q. by move/(BQ_of_nat_injective); rewrite /b (csum_nS _ iN); apply: (fusc_nz'). move:(QS_inv aq) (QS_inv bq) => iaq ibq. rewrite (BQprod_cN aN bN). rewrite (BQsum_div (QS_inv (QSp aq bq)) cq aq anz) (BQprod_inv aq bq). rewrite BQprodC (BQprodA aq iaq ibq) (BQprod_inv1 aq anz). rewrite BQsumC (BQsum_div cq QS1 bq bnz) - (BQprod_cN siN bN). rewrite (BQsum_cN (NS_prod siN bN) NS1). rewrite /b (csum_nS _ iN) - (csum_Sn _ pN) (fusc_rec_spec nN lt1). rewrite (BQprod_cN kiN aN) /BQdiv;rewrite - (BQprodA(QSp kiq aq) ibq iaq). rewrite (BQprod_ACA kiq aq ibq iaq) (BQprod_inv1 aq anz). by rewrite (BQprod_1r (QSp kiq ibq)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)