proposition: Theorem Qeq_trans x y z : x == y -> y == z -> x == z.
proof: Proof. unfold Qeq; intros XY YZ. apply Z.mul_reg_r with (QDen y); [auto with qarith|]. now rewrite Z.mul_shuffle0, XY, Z.mul_shuffle0, YZ, Z.mul_shuffle0. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool