theorem lt_max_n : ∀f.∀n. O < n → max n f < n.
#f #n #posn @(lt_O_n_elim ? posn) #m
-normalize (cases (f m)) normalize apply le_S_S //
+normalize (cases (f m)) normalize @le_S_S //
@le_max_n qed.
theorem le_to_le_max : ∀f.∀n,m.
theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) →
max n f = max n g.
#f #g #n (elim n) //
-#m #Hind #ext normalize >ext >Hind //
+#m #Hind #ext normalize >ext normalize in Hind; >Hind //
#i #ltim @ext /2/
qed.
[#n #leSO @False_ind /2/
|#n #m #Hind #leSS #b
(cases (true_or_false (f b))) #fb
- [lapply (true_min …fb) //
+ [lapply (true_min …fb) #H >H >H //
|>false_min // >false_min // @Hind /2/
]
]
[#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)
- [#ltbm >false_min /2/ @Hind //
- [#i #H #H1 @ismin /2/ | >eqt normalize //]
+ [#ltbm >false_min /2/ @Hind //
+ [#i #H #H1 @ismin /2/ | >eqt normalize //]
|#eqbm >true_min //
]
]
qed.
theorem f_min_true : ∀ f.∀n,b.
-(∃i:nat. b ≤ i ∧ i < n ∧ f i = true) → f (min n b f) = true.
+(∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true.
#f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
#Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
qed.