[O \Rightarrow m
| (S p) \Rightarrow mod_aux n n p].
-interpretation "natural remainder" 'module x y =
- (cic:/matita/library_autobatch/nat/div_and_mod/mod.con x y).
+interpretation "natural remainder" 'module x y = (mod x y).
let rec div_aux p m n : nat \def
match (leb m n) with
[O \Rightarrow S n
| (S p) \Rightarrow div_aux n n p].
-interpretation "natural divide" 'divide x y =
- (cic:/matita/library_autobatch/nat/div_and_mod/div.con x y).
+interpretation "natural divide" 'divide x y = (div x y).
theorem le_mod_aux_m_m:
\forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.