Ali Caglayan
Ali Caglayan
@ndcroos Also, the fact that you had to add funext, indicates that you still have the old `cyclic` around. I'm guessing you've already rebased, so make sure you've recompiled the...
For (1), you are on the right track. Recall that `H : grp_pow a n` is definitionally equal to `ab_mul n a`. Therefore you can use ```coq change (ab_mul n...
For (2), I would suggest that you continue with my proposal with `H2`. What @jdchristensen suggests will work when `n >= 1` however when `n = 0` we should get...
@ndcroos I think it would be best if you addressed that in its own PR. For the record, I did #2054 but closed it because it should follow what was...
You need to help Coq along a little. It doesn't see that `Int` is the underlying type of a group, so you need to write `(a : abgroup_Z)` instead.
You can write `change abgroup_Z in a.` before you use `a` or you can cast it by writing `(ab_nul n (a : abgroup_Z))`.
@jdchristensen I don't remember. I will take a closer look ASAP.
I'll reproduce the outstanding comments here so we can address them in one place: 1. Regarding line 143: > I think this argument about how `cat_coprod_prod` computes when composed with...
@jdchristensen I haven't been able to make progress with the comments that we had, perhaps I no longer understand what needs to be done. Would you be able to take...
That's fine with me @jdchristensen