search

math-comp / algebra-tactics

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

Hypothesis handling #5

Closed pi8027 closed 3 years ago

pi8027 commented 3 years ago

https://github.com/math-comp/algebra-tactics/blob/55e946113e2b1fb86ce071d5259d123803e84ec9/examples/field_examples.v#L18-L19 It would be better if we do not have to introduce the last hypothesis eq_yx, as follows:

Proof. by move=> F x y y_neq0; field; exact/eqP. Qed.