proposition: Lemma Qminus_lazy_Qminus : forall x y : Q, Qminus_lazy x y = Qminus x y.
proof: Proof. intros x y. unfold Qminus_lazy in |- *. rewrite quadratic in |- *. unfold spec_q in |- *. change (Z_to_Q 1) with Qone in |- *. unfold Z_to_Q in |- *. simpl Qpositive_c in |- *. field. discriminate. Defined.
imports: Coq(Eqdep_dec)