proposition: Theorem construct_correct : forall (w : Qpositive) (p q n : nat), Qpositive_i w = (p, q) -> p + q <= n -> Qpositive_c p q n = w.
proof: Proof. intros w; elim w; clear w. intros w'; simpl in |- *. elim (interp_non_zero w'); intros p' Hex; elim Hex; intros q' Heq. rewrite Heq. intros Hrec p q n Heq_pair. injection Heq_pair; intros Heq2 Heq1; rewrite <- Heq2; rewrite <- Heq1. case n. simpl in |- *; intros Hle; inversion Hle. clear n; intros n. intros Hle. replace (Qpositive_c (S (p' + S q')) (S q') (S n)) with (nR (Qpositive_c (S p') (S q') n)). apply f_equal with (f := nR). apply Hrec; auto with *. rewrite <- plus_Sn_m. rewrite Qpositive_c_unfold1. auto with *. auto with *. intros w'; simpl in |- *. elim (interp_non_zero w'); intros p' Hex; elim Hex; intros q' Heq. rewrite Heq. intros Hrec p q n Heq_pair. injection Heq_pair; intros Heq2 Heq1; rewrite <- Heq2; rewrite <- Heq1. case n. simpl in |- *; intros Hle; inversion Hle. clear n; intros n. intros Hle. replace (Qpositive_c (S p') (S (p' + S q')) (S n)) with (dL (Qpositive_c (S p') (S q') n)). apply f_equal with (f := dL). apply Hrec; auto with *. rewrite <- plus_Sn_m. rewrite Qpositive_c_unfold2; auto with *. simpl in |- *; intros p q n Heq; injection Heq; intros Heq2 Heq1; case n. rewrite <- Heq1; simpl in |- *; intros Hle; inversion Hle. rewrite <- Heq1; rewrite <- Heq2; simpl in |- *; auto with *. Qed.