proposition: Theorem interp_reduced_fraction : forall w : Qpositive, exists a : Z, (exists b : Z, (a * fst (Qpositive_i w) + b * snd (Qpositive_i w))%Z = 1%Z).
proof: Proof. intros w; elim w; clear w. intros w Hrec; elim Hrec; intros a Hrec2; elim Hrec2; intros b; simpl in |- *; case (Qpositive_i w); simpl in |- *. intros p q Heq; exists a; exists (b - a)%Z. rewrite <- Heq; repeat rewrite Znat.inj_plus; ring. intros w Hrec; elim Hrec; intros a Hrec2; elim Hrec2; intros b; simpl in |- *; case (Qpositive_i w); simpl in |- *. intros p q Heq; exists (a - b)%Z; exists b. rewrite <- Heq; repeat rewrite Znat.inj_plus; ring. exists 1%Z; exists 0%Z; simpl in |- *; lia. Qed.