proposition: Lemma big_pow1 x : x <> 1 -> \sum_(i < n) x ^ i.+1 = x * (1 - (x ^ n)) / (1 - x).
proof: Proof. move => neq_x_1. apply: (Rplus_eq_reg_l 1). rewrite [X in _ = X + _](_ : _ = (1 - x) / (1 - x)); last first. rewrite divRR //; apply/eqP; rewrite subR_eq0; exact/nesym. rewrite mulRDr mulR1 -mulRDl addRA [in RHS]addRC -addRA. rewrite Rplus_opp_l addR0 (addRC _ 1) mulRN. rewrite -(big_mkord xpredT (fun i => x ^ i.+1)) (_ : n = n.+1.-1) //. rewrite -(big_add1 _ _ _ _ xpredT)-{1}(pow_O x) -big_ltn //. by rewrite big_mkord -sum_f_R0_sumR tech3. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code