proposition: Lemma show_is_Qinv x q: x * q == 1 -> x == / q.
proof: Proof. intros. apply Qinv_char. assumption. Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List