An exact proof term for the current goal is CD_add_com {4} HSNo octonion_tag_fresh add_HSNo add_HSNo_com.