proposition: Theorem Qpositive_mult_inv : forall w : Qpositive, Qpositive_mult w (Qpositive_inv w) = One.
proof: Proof. intros w; elim w; clear w. intros w' Hrec; simpl in |- *. elim (interp_non_zero w'); intros p Hex; elim Hex; intros q Heq; clear Hex. unfold Qpositive_mult in |- *. simpl in |- *. rewrite (inv_correct _ _ _ Heq). rewrite Heq. simpl in |- *. replace (q + (p + S q) * S q - (q + S p + q * S (q + S p))) with 0; [ replace (q + S p + q * S (q + S p) - (q + (p + S q) * S q)) with 0; [ auto | idtac ] | idtac ]; (repeat (rewrite <- plus_n_Sm; repeat rewrite <- mult_n_Sm); simpl in |- *; match goal with | |- (0 = ?X1 - ?X2 :>nat) => replace X1 with X2; [ auto with arith | ring ] end). intros w' Hrec; simpl in |- *. elim (interp_non_zero w'); intros p Hex; elim Hex; intros q Heq; clear Hex. unfold Qpositive_mult in |- *. simpl in |- *. rewrite (inv_correct _ _ _ Heq). rewrite Heq. simpl in |- *. replace (q + S p + p * S (q + S p) - (p + (p + S q) * S p)) with 0; [ replace (p + (p + S q) * S p - (q + S p + p * S (q + S p))) with 0; [ auto | idtac ] | idtac ]; (repeat (rewrite <- plus_n_Sm; repeat rewrite <- mult_n_Sm); simpl in |- *; match goal with | |- (0 = ?X1 - ?X2 :>nat) => replace X1 with X2; [ auto with arith | ring ] end). simpl in |- *; auto. Qed.