proposition: Lemma Qopp_lazy_Qopp : forall x : Q, Qopp_lazy x = Qopp x.
proof: Proof. intros x. unfold Qopp_lazy in |- *. rewrite homography. unfold spec_h in |- *. replace (Z_to_Q 1) with Qone; trivial. replace (Z_to_Q (-1)) with (Qopp Qone); trivial. unfold Z_to_Q in |- *. rewrite Qmult_Qopp_left. rewrite Qmult_zero. rewrite Qplus_zero_right. rewrite Qplus_zero_left. rewrite Qmult_one_right. rewrite Qmult_one_left. reflexivity. Defined.
imports: Coq(Eqdep_dec)