From mathcomp Require Import all_ssreflect.

(* fintype *)

Check ord0 : 'I_1.

Goal #|'I_3| = 3.
by rewrite card_ord.
Abort.

Goal [seq val i | i <- enum 'I_3] = [:: 0; 1; 2].
rewrite enumT /=.
rewrite unlock /=.
by rewrite val_ord_enum.
Abort.

(* 名古屋大学 2013 *)

Section Nagoya2013.

Definition Sk k n :=
  \sum_(1<=i<n.+1) i^k.

Variable m : nat.
Hypothesis Hm : m > 1.

Definition Tm n :=
  \sum_(1<=k<m) 'C(m,k) * Sk k n.

Lemma Sk1 k : Sk k 1 = 1.
Proof. by rewrite /Sk big_nat1 exp1n. Qed.

Lemma Tm1 : Tm 1 = 2^m - 2.
Proof.
  rewrite /Tm.
  rewrite [in 2^m](_ : 2 = 1+1) //.
  rewrite Pascal.
  transitivity ((\sum_(0 <= k < m.+1) 'C(m,k)) - 2).
    symmetry.
    rewrite (@big_cat_nat _ _ _ m) //=.
    rewrite (@big_cat_nat _ _ _ 1) //=; last by apply ltnW.
    rewrite !big_nat1 bin0 binn addnAC addKn.
    apply eq_bigr => i H.
    by rewrite Sk1 muln1.
  rewrite big_mkord.
  congr (_ - _).
  apply eq_bigr => i _.
  by rewrite !exp1n !muln1.
Qed.

Check subn1.
Check (fun m n => addKn m n).
Check subnDA.
Check addnBA.
Check subnK.
Check prednK.
Check exp1n.
Check expn0.
Check expn1.
Check expn_gt0.
Check ltn_exp2r.
Check leq_pexp2l.

Lemma Tm2 : Tm 2 = 3^m - 3.
Proof.
  rewrite /Tm.
  have Hm': m > 0 by apply ltnW.
  have ->: 3^m - 3 = 2^m - 2 + (3^m - 1 - 2^m).
    admit.
  rewrite -Tm1.
  rewrite [in 3^m](_ : 3 = 1+2) //.
  rewrite Pascal.
  transitivity (Tm 1 + (\sum_(1 <= k < m) 'C(m,k) * 2^k)).
    rewrite -big_split /=.
    apply eq_bigr => i _.
    rewrite /Sk !big_cons !big_nil.
    by rewrite !addn0 -mulnDr.
  congr (_ + _).
  transitivity ((\sum_(0 <= k < m.+1) 'C(m,k) * 2^k) - 1 - 2^m).
Admitted.

Theorem Tmn n : Tm n.+1 = n.+2 ^ m - n.+2.
Proof.
  elim:n => [|n IHn] /=.
    by apply Tm1.
  have Hm': m > 0 by apply ltnW.
  have ->: n.+3^m - n.+3 = n.+2^m - n.+2 + (n.+3^m - 1 - n.+2^m).
Admitted.

Theorem Skp p k : p > 2 -> prime p -> 1 <= k < p.-1 -> p %| Sk k p.-1.
Admitted.

End Nagoya2013.