matita/library/nat/primes1.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 (*       \ /        Matita 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/primes1".
  16
  17 include "datatypes/constructors.ma".
  18 include "nat/primes.ma".
  19
  20 (* p is just an upper bound, acc is an accumulator *)
  21 let rec n_divides_aux p n m acc \def
  22   match n \mod m with
  23   [ O \Rightarrow
  24     match p with
  25       [ O \Rightarrow pair nat nat acc n
  26       | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
  27   | (S a) \Rightarrow pair nat nat acc n].
  28
  29 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
  30 definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.
  31
  32 (*
  33 theorem n_divides_to_Prop: \forall n,m,p,a.
  34   match n_divides_aux p n m a with
  35   [ (pair q r) \Rightarrow n = m \sup a *r].
  36 intros.
  37 apply nat_case (n \mod m). *)
  38