let n, k be Nat; :: thesis: for a, b being non trivial Nat st a,b are_congruent_mod k holds

Px (a,n), Px (b,n) are_congruent_mod k

let a, b be non trivial Nat; :: thesis: ( a,b are_congruent_mod k implies Px (a,n), Px (b,n) are_congruent_mod k )

assume a,b are_congruent_mod k ; :: thesis: Px (a,n), Px (b,n) are_congruent_mod k

then consider x being Integer such that

A1: k * x = a - b by INT_1:def 5;

consider p being Integer such that

A2: (a - b) * p = (Px (a,n)) - (Px (b,n)) by HILB10_1:25, INT_1:def 5;

p * (a - b) = p * (x * k) by A1

.= (p * x) * k ;

hence Px (a,n), Px (b,n) are_congruent_mod k by A2, INT_1:def 5; :: thesis: verum

Px (a,n), Px (b,n) are_congruent_mod k

let a, b be non trivial Nat; :: thesis: ( a,b are_congruent_mod k implies Px (a,n), Px (b,n) are_congruent_mod k )

assume a,b are_congruent_mod k ; :: thesis: Px (a,n), Px (b,n) are_congruent_mod k

then consider x being Integer such that

A1: k * x = a - b by INT_1:def 5;

consider p being Integer such that

A2: (a - b) * p = (Px (a,n)) - (Px (b,n)) by HILB10_1:25, INT_1:def 5;

p * (a - b) = p * (x * k) by A1

.= (p * x) * k ;

hence Px (a,n), Px (b,n) are_congruent_mod k by A2, INT_1:def 5; :: thesis: verum