Kazuhiko Sakaguchi

@fajb Thank you for great work. If it does work, we don't need to manipulate the goal twice anymore!

I have started to implement the class instances to make `zify` does work for `ssrnat` and `ssrint` and see some issues: - `zify` doesn't work for overloaded operators, e.g., `@eq_op...

(For the record, I reported the above issue of the anomaly as coq/coq#10779. It will be fixed by coq/coq#10787.)

I have declared `zify` class instances for `ssrbool`, `ssrnat`, and `div`. Instances for `ssrint` and `intdiv` are not done yet. https://github.com/pi8027/mczify/blob/master/theories/zify.v

I finished defining instances for most definitions on `bool`, `nat`, and `int` in MathComp, including `gcdn`, `lcmn`, `coprime`, `divz`, `dvdz`, `gcdz`, `coprimez`, etc. but excluding `factorial`, `modz`, and definitions in...

I did some improvements on `(div|mod|dvd)(n|z)`. Now micromega tactics can prove the following lemmas: ```coq Lemma dvdz_lcm_6_4 (m : int) : (6 %| m -> 4 %| m -> 12...

I hope the extensible `zify` tactic will be stable enough in Coq 8.13 thanks to coq/coq#11906 and it will make it easier to support several combinations of versions of Coq...

Without `seq_eqclass`, `pred_of_seq` has type `forall (T : eqType), seq (Equality.sort T) -> {pred T}`, thus is not uniform.

I thought there would be an intermediate structure between integral domains and fields (such as Euclidean domains) that subsumes these concepts of division operators. However, `divp` is not a Euclidean...

There was a similar discussion on Gitter. I just repeat my comment: > I think there are at least two technical reasons here. The group structure without finiteness should be...