]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/library_auto/auto/nat/div_and_mod.ma
Ported demodulation on clauses
[helm.git] / helm / software / matita / contribs / library_auto / auto / nat / div_and_mod.ma
index bbb3d49b1c32a13721e9bc3b996d628aedd9f6a4..d81a0a1cf8c127c413334d26b3241637fb21198b 100644 (file)
@@ -31,8 +31,7 @@ match m with
 [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
@@ -48,8 +47,7 @@ match m 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.