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 ;
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 ;
0 + (v . b) <= (v . (a / b)) + (v . b) by ;
hence v . b <= v . a by ; :: thesis: verum
end;
end;