proof ok

prelude/nat_ops.lp

-require open pvs_core prelude.notequal prelude.nat
+require open pvs_core prelude.notequal prelude.nat prelude.equalities
 symbol times : eta int ⇒ eta int ⇒ eta int
-rule times &n 1 → &n
+rule times &n 1  → &n
+
+set infix left 6 "*" ≔ times
 
 // x =/= 0 ∧ y =/= 0 ⇒ x * y =/= 0
 symbol prod_not_zero (x y: eta int) :
   eps (neq x 0) ⇒ eps (neq y 0) ⇒ eps (neq (times x y) 0)
+
+symbol prod_comm (x y : eta int) : eps (eq (x * y) (y * x))

prelude/rat.lp

@@ -19,8 +19,11 @@ symbol rateq : eta rat ⇒ eta rat ⇒ eta Prop
 rule rateq (frac &A &B &Pi) (frac &C &D &Pi') →
   eq (N.times &A &D) (N.times &B &C)
 
-theorem t1 : ∀ a b : eta int, ∀ pi : eps (neq b 0), ∀ pi' : eps (neq 1 0),
+// (a/b) * (b/1) = (a/1)
+theorem right_cancellation (a b : eta int) (pi : eps (neq b 0)) (pi' : eps (neq 1 0)):
   eps (rateq ((frac a b pi) * (frac b 1 pi')) (frac a 1 pi'))
 proof
 assume a b pi pi'
-admit
+simpl
+refine N.prod_comm a b
+qed