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;

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

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

then v . a = +infty by A1, Def8;
hence v . b <= v . a by XXREAL_0:3; :: thesis: verum

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;

end;