proposition: Lemma Qinv_is_inv : forall (x : Q) (Hx : x/=0), (x*Qinv_dep x Hx==1) /\ (Qinv_dep x Hx*x==1).
proof: Proof. intros x Hx. split. now apply (Qmult_inv_r x). rewrite -> Qmult_comm. now apply (Qmult_inv_r x). Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q