proposition: Theorem Qplus_assoc : forall x y z, x+(y+z)==(x+y)+z.
proof: Proof. intros (x1, x2) (y1, y2) (z1, z2). unfold Qeq, Qplus; simpl; simpl_mult; ring. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool