let a be non trivial Nat; :: thesis: for b, c being non zero Integer st a |^ (a |-count b) divides c & a |^ (a |-count c) divides b holds
a |-count b = a |-count c
let b, c be non zero Integer; :: thesis: ( a |^ (a |-count b) divides c & a |^ (a |-count c) divides b implies a |-count b = a |-count c )
assume ( a |^ (a |-count b) divides c & a |^ (a |-count c) divides b ) ; :: thesis: a |-count b = a |-count c
then ( a |-count b >= a |-count c & a |-count b <= a |-count c ) by DL;
hence a |-count b = a |-count c by XXREAL_0:1; :: thesis: verum