proposition: Theorem Qnum_inv : ∀ a, (0 < Qnum a)%Z → Qnum (/ a) = Zpos (Qden a).
proof: Proof. intros (a, b) Ha; simpl in Ha |- *. unfold Qinv; simpl. destruct a as [| a| a]; simpl. apply Z.lt_irrefl in Ha; contradiction. reflexivity. apply Zlt_not_le in Ha. exfalso; apply Ha, Z.lt_le_incl, Zlt_neg_0. Qed.
imports: Utf8 QArith NPeano Sorted Psatz