permutation.ma added to the repository.

[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 ba3151a3b34ce7da6f27148ab193d50abe6680b5..55e526c8fad0f80eade4775141c99326975efee8 100644 (file)
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -64,6 +64,25 @@ apply (H H2).
 apply (H1 H2).
 qed.
 
+theorem eqb_n_n: \forall n. eqb n n = true.
+intro.elim n.simplify.reflexivity.
+simplify.assumption.
+qed.
+
+theorem eq_to_eqb_true: \forall n,m:nat.
+n = m \to eqb n m = true.
+intros.apply eqb_elim n m.
+intros. reflexivity.
+intros.apply False_ind.apply H1 H.
+qed.
+
+theorem not_eq_to_eqb_false: \forall n,m:nat.
+\lnot (n = m) \to eqb n m = false.
+intros.apply eqb_elim n m.
+intros. apply False_ind.apply H H1.
+intros.reflexivity.
+qed.
+
 let rec leb n m \def 
 match n with 
     [ O \Rightarrow true