include "arithmetics/sigma_pi.ma".
include "arithmetics/bounded_quantifiers.ma".
include "reverse_complexity/big_O.ma".
+include "basics/core_notation/napart_2.ma".
(************************* notation for minimization *****************************)
notation "μ_{ ident i < n } p"
h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
#r #a #b normalize >fst_pair >snd_pair //
qed.
-
-(* (∀x.MSC x≤h (S (fst x)) (snd(snd x))) → *)
lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
@Hmono @(mono_h_of2 … Hr Hmono … ltin)
]
qed.
-
\ No newline at end of file
+