let p be Prime; :: thesis: for a, b being non zero Nat st b divides a holds
p |-count b <= p |-count a
let a, b be non zero Nat; :: thesis: ( b divides a implies p |-count b <= p |-count a )
set x = p |-count a;
set y = p |-count b;
set z = p |-count (a div b);
0 + 1 <= p |^ (p |-count (a div b)) by NAT_1:13;
then A1: 1 * (p |^ (p |-count b)) <= (p |^ (p |-count (a div b))) * (p |^ (p |-count b)) by XREAL_1:66;
assume b divides a ; :: thesis: p |-count b <= p |-count a
then A2: a = b * (a div b) by NAT_D:3;
then a div b <> 0 ;
then ( p > 1 & p |^ (p |-count b) <= p |^ (p |-count a) ) by A2, A1, Th29, INT_2:def 4;
hence p |-count b <= p |-count a by PEPIN:66; :: thesis: verum