begin
:: deftheorem Def1 defines are_relative_prime PYTHTRIP:def 1 :
:: deftheorem Def2 defines are_relative_prime PYTHTRIP:def 2 :
begin
:: deftheorem Def3 defines square PYTHTRIP:def 3 :
theorem Th1:
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
begin
theorem Th7:
theorem Th8:
begin
theorem Th9:
begin
theorem Th10:
theorem Th11:
theorem
:: deftheorem Def4 defines Pythagorean_triple PYTHTRIP:def 4 :
:: deftheorem Def5 defines Pythagorean_triple PYTHTRIP:def 5 :
:: deftheorem Def6 defines degenerate PYTHTRIP:def 6 :
theorem
:: deftheorem Def7 defines simplified PYTHTRIP:def 7 :
:: deftheorem Def8 defines simplified PYTHTRIP:def 8 :
theorem Th14:
theorem
theorem