(* 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 *)
match n_divides_aux p n m a with
[ (pair q r) \Rightarrow n = m \sup a *r].
intros.
-apply nat_case (mod n m). *)
+apply nat_case (n \mod m). *)