diff options
| -rw-r--r-- | theories/QArith/Qfield.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index 3b14a47ce..4d8a80611 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -70,6 +70,8 @@ Ltac Qcst t := Ltac Qpow_tac t := match t with + | Z0 => N0 + | Zpos ?n => Ncst (Npos n) | Z_of_N ?n => Ncst n | NtoZ ?n => Ncst n | _ => NotConstant @@ -112,6 +114,16 @@ Let ex7 : forall x : Q, x-x== 0#1. ring. Qed. +Let ex8 : forall x : Q, x^1 == x. + intro. + ring. +Qed. + +Let ex9 : forall x : Q, x^0 == 1. + intro. + ring. +Qed. + Example test_field : forall x y : Q, ~(y==0) -> (x/y)*y == x. intros. field. |