let
a
,
b
be
Nat
;
:: thesis:
(
a
<=
b
implies
seq_n^
a
in
Big_Oh
(
seq_n^
b
)
)
assume
AS
:
a
<=
b
;
:: thesis:
seq_n^
a
in
Big_Oh
(
seq_n^
b
)
per
cases
(
a
=
b
or
a
<
b
)
by
AS
,
XXREAL_0:1
;
suppose
a
=
b
;
:: thesis:
seq_n^
a
in
Big_Oh
(
seq_n^
b
)
hence
seq_n^
a
in
Big_Oh
(
seq_n^
b
)
by
ASYMPT_0:10
;
:: thesis:
verum
end;
suppose
a
<
b
;
:: thesis:
seq_n^
a
in
Big_Oh
(
seq_n^
b
)
hence
seq_n^
a
in
Big_Oh
(
seq_n^
b
)
by
FROMASYMPT1t11
;
:: thesis:
verum
end;
end;