proposition: Theorem Qinv_def : forall x : Q, x <> Zero -> Qmult x (Qinv x) = Qpos One.
proof: Proof. intros x; case x. 2: intros x' Hneg; simpl in |- *. 2: rewrite Qpositive_mult_inv; auto. intros H; elim H; auto. intros x' Hneg; simpl in |- *. rewrite Qpositive_mult_inv; auto. Qed.