proposition: Theorem inv_correct : forall (w : Qpositive) (p q : nat), Qpositive_i w = (p, q) -> Qpositive_i (Qpositive_inv w) = (q, p).
proof: Proof. let T_local := (intros w'; simpl in |- *; case (Qpositive_i w'); intros p' q' Hrec p q Heq; rewrite (Hrec p' q'); auto; injection Heq; intros H1 H2; rewrite <- H1; rewrite <- H2; rewrite Nat.add_comm; auto) in (intros w; elim w; clear w; [ T_local | T_local | simpl in |- *; intros p q Heq; injection Heq; intros H1 H2; rewrite <- H1; rewrite <- H2; auto with * ]). Qed.