proposition: Lemma Qplus_lazy_Qplus : forall x y : Q, Qplus_lazy x y = Qplus x y.
proof: Proof. intros x y. unfold Qplus_lazy in |- *. rewrite quadratic. unfold spec_q in |- *. replace (Z_to_Q 1) with Qone; trivial. unfold Z_to_Q in |- *. repeat rewrite Qmult_one_left. rewrite Qmult_one_right. repeat rewrite Qmult_zero. rewrite Qplus_zero_left. rewrite Qplus_zero_right. reflexivity. Defined.
imports: Coq(Eqdep_dec)