Section Examples.
Let ex1 :
forall x y z :
Q, (
x+y)*z == (
x*z)+(y*z).
Qed.
Let ex2 :
forall x y :
Q,
x+y ==
y+x.
Qed.
Let ex3 :
forall x y z :
Q, (
x+y)+z ==
x+(y+z).
Qed.
Let ex4 : (
inject_Z 1)+(inject_Z 1)==(inject_Z 2).
Qed.
Let ex5 : 1+1 == 2#1.
Qed.
Let ex6 : (1#1)+(1#1) == 2#1.
Qed.
Let ex7 :
forall x :
Q,
x-x== 0.
Qed.
Let ex8 :
forall x :
Q,
x^1 ==
x.
Qed.
Let ex9 :
forall x :
Q,
x^0 == 1.
Qed.
Let ex10 :
forall x y :
Q, ~(y==0) -> (
x/y)*y ==
x.
Qed.
End Examples.
Lemma Qopp_plus :
forall a b, -(a+b) == -a + -b.
Lemma Qopp_opp :
forall q, - -q==q.