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