search

coq-community / coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Other
65 stars 17 forks source link

refactor proofs in theory #69

Closed clayrat closed 1 year ago

clayrat commented 1 year ago

Trim down some proofs (mostly by using contraposition and eqVneq), re-use lt_wf in dvdring.v, some formatting and syntactic sugar.

clayrat commented 1 year ago

@proux01 I've tried to de-noise a bit by removing case/orP, case/andP, rewrite + apply/exact combinations and explicit branch handling, tell me if more is needed.

proux01 commented 1 year ago

@clayrat thanks a lot. I updated a few more details (spacing (particularly around =>), by apply: replaced by exact:). If it is good for you, I'll squash and merge.

clayrat commented 1 year ago

@proux01 sure, thank you too!