let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a, b being Element of K

for v being Valuation of K st K is having_valuation & b <> 0. K & 0 <= v . (a / b) holds

v . b <= v . a

let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & b <> 0. K & 0 <= v . (a / b) holds

v . b <= v . a

let v be Valuation of K; :: thesis: ( K is having_valuation & b <> 0. K & 0 <= v . (a / b) implies v . b <= v . a )

assume that

A1: K is having_valuation and

A2: b <> 0. K and

A3: 0 <= v . (a / b) ; :: thesis: v . b <= v . a

A4: v . (a / b) = (v . a) - (v . b) by A1, A2, Th22;

for v being Valuation of K st K is having_valuation & b <> 0. K & 0 <= v . (a / b) holds

v . b <= v . a

let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & b <> 0. K & 0 <= v . (a / b) holds

v . b <= v . a

let v be Valuation of K; :: thesis: ( K is having_valuation & b <> 0. K & 0 <= v . (a / b) implies v . b <= v . a )

assume that

A1: K is having_valuation and

A2: b <> 0. K and

A3: 0 <= v . (a / b) ; :: thesis: v . b <= v . a

A4: v . (a / b) = (v . a) - (v . b) by A1, A2, Th22;

per cases
( a = 0. K or a <> 0. K )
;

end;

suppose
a <> 0. K
; :: thesis: v . b <= v . a

then
( v . a in INT & v . b in INT )
by A1, A2, Def8;

then reconsider a1 = v . a, b1 = v . b as Element of REAL by XREAL_0:def 1;

A5: (a1 - b1) + b1 = a1 ;

a1 - b1 = (v . a) - (v . b) by Lm1;

then A6: (v . (a / b)) + (v . b) = v . a by A4, A5, XXREAL_3:def 2;

0 + (v . b) <= (v . (a / b)) + (v . b) by A3, XXREAL_3:35;

hence v . b <= v . a by A6, XXREAL_3:4; :: thesis: verum

end;then reconsider a1 = v . a, b1 = v . b as Element of REAL by XREAL_0:def 1;

A5: (a1 - b1) + b1 = a1 ;

a1 - b1 = (v . a) - (v . b) by Lm1;

then A6: (v . (a / b)) + (v . b) = v . a by A4, A5, XXREAL_3:def 2;

0 + (v . b) <= (v . (a / b)) + (v . b) by A3, XXREAL_3:35;

hence v . b <= v . a by A6, XXREAL_3:4; :: thesis: verum