proposition: Theorem interp_non_zero : forall w : Qpositive, exists p : nat, (exists q : nat, Qpositive_i w = (S p, S q)).
proof: Proof. simple induction w; simpl in |- *; (repeat exists 0; auto; fail) || (intros w' Hrec; elim Hrec; intros p' Hex; elim Hex; intros q' Heq; rewrite Heq). exists (p' + S q'); exists q'; auto. exists p'; exists (p' + S q'); auto. Qed.