Totient function and related files.

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

diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index 6431f5f293e219fcc5af7ebe84c315c4da5d0ae4..e85a802652e9ce8ba67d3b6b511eaf5b06bc6ea3 100644 (file)
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -69,6 +69,28 @@ intro.elim n.simplify.reflexivity.
 simplify.assumption.
 qed.
 
+theorem eqb_true_to_eq: \forall n,m:nat.
+eqb n m = true \to n = m.
+intros.
+change with 
+match true with
+[ true  \Rightarrow n = m 
+| false \Rightarrow n \neq m].
+rewrite < H.
+apply eqb_to_Prop. 
+qed.
+
+theorem eqb_false_to_not_eq: \forall n,m:nat.
+eqb n m = false \to n \neq m.
+intros.
+change with 
+match false with
+[ true  \Rightarrow n = m 
+| false \Rightarrow n \neq m].
+rewrite < H.
+apply eqb_to_Prop. 
+qed.
+
 theorem eq_to_eqb_true: \forall n,m:nat.
 n = m \to eqb n m = true.
 intros.apply (eqb_elim n m).