let b be non zero Nat; :: thesis: for a being non trivial Nat holds
( a |-count (a gcd b) = 0 iff not a |-count (a gcd b) = 1 )
let a be non trivial Nat; :: thesis: ( a |-count (a gcd b) = 0 iff not a |-count (a gcd b) = 1 )
reconsider c = a gcd b as non zero Nat ;
a > 1 by Def0;
then L1: ( a |-count (a gcd b) = 0 iff not a divides a gcd b ) by NAT_3:27;
a gcd b divides b by INT_2:def 2;
hence ( a |-count (a gcd b) = 0 iff not a |-count (a gcd b) = 1 ) by CD, INT_2:9, L1; :: thesis: verum