proposition: Lemma Qmult_lazy_Qmult : forall x y : Q, Qmult_lazy x y = Qmult x y.
proof: Proof. intros x y. unfold Qmult_lazy in |- *. rewrite quadratic. unfold spec_q in |- *. change (Z_to_Q 1) with Qone. unfold Z_to_Q in |- *. rewrite Qmult_one_left. rewrite Qmult_one_right. repeat rewrite Qmult_zero. repeat rewrite Qplus_zero_right. repeat rewrite Qplus_zero_left. reflexivity. Defined.
imports: Coq(Eqdep_dec)