Few theorems added.`

[helm.git] / matita / library / nat / div_and_mod.ma

diff --git a/matita/library/nat/div_and_mod.ma b/matita/library/nat/div_and_mod.ma
index 73ff78998bce36d1edaff044378b0145fc0a8940..ccddcca3f14416507c5edabf52e985dbf7757a68 100644 (file)
--- a/matita/library/nat/div_and_mod.ma
+++ b/matita/library/nat/div_and_mod.ma
@@ -28,7 +28,7 @@ match (leb m n) with
 definition mod : nat \to nat \to nat \def
 \lambda n,m.
 match m with 
-[O \Rightarrow m
+[O \Rightarrow n
 | (S p) \Rightarrow mod_aux n n p]. 
 
 interpretation "natural remainder" 'module x y =
@@ -143,7 +143,7 @@ rewrite > distr_times_minus.
 rewrite > plus_minus.
 rewrite > sym_times.
 rewrite < H5.
-rewrite < sym_times.
+rewrite < sym_times. 
 apply plus_to_minus.
 apply H3.
 apply le_times_r.