proposition: Lemma total_Qinv_lazy_defT : forall n : Q, n <> Zero -> Qmult_lazy (total_Qinv_lazy n) n = Qone.
proof: Proof. intros n Hn. unfold total_Qinv_lazy in |- *; case (Q_zerop n); intros Hn'; [ Falsum | apply Qinv_lazy_defT ]. Defined.
imports: Coq(Eqdep_dec)