proposition: Lemma Tnk2_sum n k: k < n -> (n-k)`!*(n+k+2)`! * ((Tnk2 n k) + (Tnk2 n k.+1)) = (n.*2.+1)`! * k.*2.+2.
proof: Proof. move=> lkn; move:(lkn); rewrite - (subn_gt0) => ha. have eq3: (n - k) `! = (n-k) * (n - k.+1)`! by rewrite - (prednK ha) factS subnS. have eq4:= (subnK (ltnW lkn)). rewrite mulnDr {1} addnS factS (mulnCA) - mulnA (Tnk2_div2 (ltnW lkn)) addnC. rewrite eq3 - 2!(mulnA (n- k)) addn2 -addnS - (addn1 (_ + _)) (Tnk2_div2 lkn). rewrite mulnCA (mulnCA _ (n.*2)`!) - mulnDr factSr addn1 -{3} eq4 -addnA. rewrite addnn -2! addnS mulnDl addnA -mulnDr addSnnS - doubleS addnn. rewrite (mulnC (k.+1).*2) -(mul2n ((k.+1).*2)) mulnA -mulnDl addnS -(muln2 k). by rewrite - mulnDl eq4 muln2 mulnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)