proposition: Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1.
proof: Proof. intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl; intros H **; simpl_mult; try ring. elim H; auto. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool