Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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 1. Definition Tm n := \sum_(1<=k 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.