helm/matita/library/nat/fermat_little_theorem.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/fermat_little_theorem".
  16
  17 include "nat/gcd.ma".
  18 include "nat/permutation.ma".
  19
  20 theorem permut_mod: \forall p,a:nat. prime p \to
  21 \lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p).
  22 unfold permut.intros.
  23 split.intros.apply le_S_S_to_le.
  24 apply trans_le ? p.
  25 change with mod (a*i) p < p.
  26 apply lt_mod_m_m.
  27 simplify in H.elim H.
  28 simplify.apply trans_le ? (S (S O)).
  29 apply le_n_Sn.assumption.
  30 rewrite < S_pred.apply le_n.
  31 unfold prime in H.
  32 elim H.
  33 apply trans_lt ? (S O).simplify.apply le_n.assumption.
  34 unfold injn.intros.
  35 apply nat_compare_elim i j.
  36 (* i < j *)
  37 intro.
  38 absurd j-i \lt p.
  39 simplify.
  40 rewrite > S_pred p.
  41 apply le_S_S.
  42 apply le_plus_to_minus.
  43 apply trans_le ? (pred p).assumption.
  44 rewrite > sym_plus.
  45 apply le_plus_n.
  46 unfold prime in H.
  47 elim H.
  48 apply trans_lt ? (S O).simplify.apply le_n.assumption.
  49 apply le_to_not_lt p (j-i).
  50 apply divides_to_le.simplify.
  51 apply le_SO_minus.assumption.
  52 cut divides p a \lor divides p (j-i).
  53 elim Hcut.apply False_ind.apply H1.assumption.assumption.
  54 apply divides_times_to_divides.assumption.
  55 rewrite > distr_times_minus.
  56 apply eq_mod_to_divides.
  57 unfold prime in H.
  58 elim H.
  59 apply trans_lt ? (S O).simplify.apply le_n.assumption.
  60 apply sym_eq.
  61 apply H4.
  62 (* i = j *)
  63 intro. assumption.
  64 (* j < i *)
  65 intro.
  66 absurd i-j \lt p.
  67 simplify.
  68 rewrite > S_pred p.
  69 apply le_S_S.
  70 apply le_plus_to_minus.
  71 apply trans_le ? (pred p).assumption.
  72 rewrite > sym_plus.
  73 apply le_plus_n.
  74 unfold prime in H.
  75 elim H.
  76 apply trans_lt ? (S O).simplify.apply le_n.assumption.
  77 apply le_to_not_lt p (i-j).
  78 apply divides_to_le.simplify.
  79 apply le_SO_minus.assumption.
  80 cut divides p a \lor divides p (i-j).
  81 elim Hcut.apply False_ind.apply H1.assumption.assumption.
  82 apply divides_times_to_divides.assumption.
  83 rewrite > distr_times_minus.
  84 apply eq_mod_to_divides.
  85 unfold prime in H.
  86 elim H.
  87 apply trans_lt ? (S O).simplify.apply le_n.assumption.
  88 apply H4.
  89 qed.
  90