search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

Simplify non-zero conditions of the field tactic #19

Closed pi8027 closed 3 years ago

pi8027 commented 3 years ago

Fixes #13

For example,

Goal forall (F : fieldType), - 10%:R / (10%:R / - 1%:R) = 1 :> F.
Proof.
move=> F; field.

now produces

  F : fieldType
  ============================
  10%:~R != 0

subgoal 2 (ID 7374) is:
 (Negz 0)%:~R != 0
pi8027 commented 3 years ago

Subgoal 2 in the example above is not quite satisfactory though.