From 7ee82ad8d5f0b78674694826d2a0bb16508b3da4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 6 Jun 2008 10:35:16 +0000 Subject: [PATCH] A new theorem --- helm/software/matita/library/nat/minimization.ma | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/helm/software/matita/library/nat/minimization.ma b/helm/software/matita/library/nat/minimization.ma index d2cde9b67..bc2cc7059 100644 --- a/helm/software/matita/library/nat/minimization.ma +++ b/helm/software/matita/library/nat/minimization.ma @@ -366,6 +366,22 @@ apply not_eq_true_false. reflexivity. qed. +theorem f_min_true: \forall f:nat \to bool. \forall m:nat. +(\exists i. le i m \land f i = true) \to +f (min m f) = true. +intros.unfold min. +apply f_min_aux_true. +elim H.clear H.elim H1.clear H1. +apply (ex_intro ? ? a). +split + [split + [apply le_O_n + |rewrite < plus_n_O.assumption + ] + |assumption + ] +qed. + theorem lt_min_aux_to_false : \forall f:nat \to bool. \forall n,off,m:nat. n \leq m \to m < (min_aux off n f) \to f m = false. intros 3. -- 2.39.2