proposition: Lemma exp3_addn1 a: (a.+1) ^3 = a^3 + a^2 *3 + a * 3 + 1.
proof: Proof. by rewrite -addn1 exp3_addn !muln1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)