for A being Ordinal holds 1,A are_coprime by ORDINAL3:37;