-theorem f_min_true : ∀ f.∀n,b.
-(∃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/
+\ 5img class="anchor" src="icons/tick.png" id="f_min_true"\ 6theorem f_min_true : ∀ f.∀n,b.
+(∃i:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → f (\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#f #n #b cases(\ 5a href="cic:/matita/arithmetics/minimization/min_to_min_spec.def(10)"\ 6min_to_min_spec\ 5/a\ 6 f n b (\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) //
+#Hall * #x * * #leb #ltx #fx @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … fx) >Hall /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"\ 6eqnot_to_noteq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="lt_min"\ 6theorem lt_min : ∀ f.∀n,b.
+(∃i:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b.
+#f #n #b #H cases H #i * * #lebi #ltin #fi_true
+@(\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"\ 6le_to_lt_to_lt\ 5/a\ 6 … ltin) @\ 5a href="cic:/matita/arithmetics/minimization/true_to_le_min.def(6)"\ 6true_to_le_min\ 5/a\ 6 //