proposition: Lemma Qinv_lazy_defT : forall (n : Q) (Hn : n <> Zero), Qmult_lazy (Qinv_lazy n Hn) n = Qone.
proof: Proof. intros n Hn; rewrite Qinv_lazy_Qinv; rewrite Qmult_lazy_Qmult; rewrite Qmult_sym; apply Qinv_def; intro; apply Hn; assumption. Defined.
imports: Coq(Eqdep_dec)