Totient function and related files.

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

diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma
index bc60b50aca084c6514d47c9565cafb94d00a1b4c..94e4ee367a605dd48b41bab97d28986044368b45 100644 (file)
--- a/helm/matita/library/nat/minimization.ma
+++ b/helm/matita/library/nat/minimization.ma
@@ -209,3 +209,14 @@ apply le_n_Sn.
 assumption.
 qed.
 
+theorem le_min_aux_r : \forall f:nat \to bool. 
+\forall n,off:nat. (min_aux off n f) \le n.
+intros.
+elim off.simplify.rewrite < minus_n_O.
+elim (f n).simplify.apply le_n.
+simplify.apply le_n.
+simplify.elim (f (n -(S n1))).
+simplify.apply le_plus_to_minus.
+rewrite < sym_plus.apply le_plus_n.
+simplify.assumption.
+qed.