proposition: Theorem RPascal k (a b : R) : (a + b) ^ k = \sum_(i < k.+1) INR ('C(k, i))* (a ^ (k - i) * b ^ i).
proof: Proof. rewrite addRC Binomial.binomial sum_f_R0_sumR. apply eq_bigr => i _. rewrite combinaisonE; last by rewrite -ltnS. rewrite -minusE; field. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)