proposition: Lemma exp3_addn a b: (a+b) ^3 = a^3 + a^2 *b *3 + a*b^2 * 3 + b^3.
proof: Proof. rewrite expnS sqrnD mulnDl 4!mulnDr. have ->: a * (2 * (a * b)) = a^2 *b *2. by rewrite -mulnA -mulnA (mulnA a b 2) (mulnC 2). have ->: b * (2 * (a * b)) = a * b ^ 2 * 2. by rewrite mulnC - mulnA (mulnC 2) mulnA. rewrite -expnS -expnS (addnAC _ (b^3)) addnA; congr (_ + _). rewrite - 3 !addnA; congr (_ + _). rewrite addnC addnA -addnA (mulnC b); congr (_ + _). by rewrite - (addn1 2) mulnDr muln1. by rewrite - (addn1 2) mulnDr muln1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)