lemma max_not_exists: ∀f.∀n.
(∀i. i < n → f i = false) → max n f = O.
#f #n #ffalse @(le_gen ? n) #i (elim i) // #j #Hind #ltj
lemma max_not_exists: ∀f.∀n.
(∀i. i < n → f i = false) → max n f = O.
#f #n #ffalse @(le_gen ? n) #i (elim i) // #j #Hind #ltj
|(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/
qed.
theorem f_max_true : ∀ f.∀n.
(∃i:nat. i < n ∧ f i = true) → f (max n f) = true.
#f #n cases(max_to_max_spec f n (max n f) (refl …)) //
|(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/
qed.
theorem f_max_true : ∀ f.∀n.
(∃i:nat. i < n ∧ f i = true) → f (max n f) = true.
#f #n cases(max_to_max_spec f n (max n f) (refl …)) //
[#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
@lt_to_not_le //
|#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
[#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
@lt_to_not_le //
|#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
lemma min_not_exists: ∀f.∀n,b.
(∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b.
#f #n (elim n) //
lemma min_not_exists: ∀f.∀n,b.
(∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b.
#f #n (elim n) //
inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝
| found : ∀m:nat. b ≤ m → m < n + b → f m =true →
inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝
| found : ∀m:nat. b ≤ m → m < n + b → f m =true →
theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) →
min n b f = min n b g.
#f #g #n (elim n) //
theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) →
min n b f = min n b g.
#f #g #n (elim n) //
|(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi
@ext /2/
qed.
theorem f_min_true : ∀ f.∀n,b.
|(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi
@ext /2/
qed.
theorem f_min_true : ∀ f.∀n,b.