(* p is just an upper bound, acc is an accumulator *)
let rec n_divides_aux p n m acc \def
- match (mod n m) with
+ match n \mod m with
[ O \Rightarrow
match p with
[ O \Rightarrow pair nat nat acc n
- | (S p) \Rightarrow n_divides_aux p (div n m) m (S acc)]
+ | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
| (S a) \Rightarrow pair nat nat acc n].
(* n_divides n m = <q,r> if m divides n q times, with remainder r *)
(*
theorem n_divides_to_Prop: \forall n,m,p,a.
match n_divides_aux p n m a with
- [ (pair q r) \Rightarrow n = (exp m a)*r].
+ [ (pair q r) \Rightarrow n = m \sup a *r].
intros.
-apply nat_case (mod n m). *)
+apply nat_case (n \mod m). *)