let
n
,
m
,
k
be
Nat
;
:: thesis:
(
m
<=
k
&
n
<
m
implies
k
'
m
<
k
'
n
)
assume
that
A1
:
m
<=
k
and
A2
:
n
<
m
;
:: thesis:
k
'
m
<
k
'
n
A3
:
k

m
<
k

n
by
A2
,
XREAL_1:15
;
k
'
n
=
k

n
by
A1
,
A2
,
XREAL_1:233
,
XXREAL_0:2
;
hence
k
'
m
<
k
'
n
by
A1
,
A3
,
XREAL_1:233
;
:: thesis:
verum