for a, b, c being natural Ordinal holds (a *^ c) hcf (b *^ c) = (a hcf b) *^ c