let n be Nat; :: thesis: ( not n is even or n, 0 are_congruent_mod 4 or n,2 are_congruent_mod 4 )
assume n is even ; :: thesis: ( n, 0 are_congruent_mod 4 or n,2 are_congruent_mod 4 )
then ( n mod 4 = 0 or n mod 4 = 2 ) by Th78;
then ( n mod 4 = 0 mod 4 or n mod 4 = 2 mod 4 ) ;
hence ( n, 0 are_congruent_mod 4 or n,2 are_congruent_mod 4 ) by NAT_D:64; :: thesis: verum