proposition: Lemma Qinv_lazy_Qinv : forall (x : Q) (Hx : x <> Zero), Qinv_lazy x Hx = Qinv x.
proof: Proof. intros x Hx. unfold Qinv_lazy in |- *. rewrite homography. unfold spec_h in |- *. replace (Z_to_Q 1) with Qone; trivial. unfold Z_to_Q in |- *. repeat rewrite Qmult_one_left. rewrite Qplus_zero_right. reflexivity. Defined.
imports: Coq(Eqdep_dec)