proposition: Theorem Qpositive_sub_correct : forall w w' : Qpositive, Qpositive_sub (Qpositive_plus w w') w' = w.
proof: Proof. intros w w'. elim (interp_non_zero w); intros p Hex; elim Hex; intros q Heq; clear Hex. elim (interp_non_zero w'); intros p' Hex; elim Hex; intros q' Heq'; clear Hex. unfold Qpositive_sub, Qpositive_plus in |- *. rewrite Heq; rewrite Heq'. elim (construct_correct2' (S p * S q' + S p' * S q + S q * S q') (S p * S q' + S p' * S q) (S q * S q')). intros d; elim (interp_non_zero (Qpositive_c (S p * S q' + S p' * S q) (S q * S q') (S p * S q' + S p' * S q + S q * S q'))); intros p3 Hex; elim Hex; intros q3 Heq3; rewrite Heq3; intros (Heq1, Heq2); clear Hex. rewrite <- (construct_correct _ _ _ (S p + S q) Heq). apply construct_correct4'; try (simpl in |- *; auto with arith; fail). unfold fst, snd in Heq1, Heq2. apply Nat.le_succ_l. apply lt_mult_conv with d. rewrite <- mult_n_O. unfold lt in |- *. rewrite (Nat.mul_comm (S d)). rewrite Nat.mul_sub_distr_r. rewrite (Nat.mul_comm (S p3)); repeat rewrite <- Nat.mul_assoc. rewrite <- Heq2; rewrite <- Heq1. rewrite (Nat.mul_comm (S q')); rewrite Nat.mul_add_distr_r. rewrite Nat.add_comm. rewrite <- Nat.mul_assoc. rewrite Nat.add_comm. rewrite Nat.add_sub. simpl in |- *; auto with arith. apply Nat.add_le_mono_r. rewrite <- Nat.le_add_r. apply Nat.le_sub_l. unfold fst, snd in Heq1, Heq2. apply mult_reg_l with d. rewrite Nat.mul_sub_distr_r; rewrite (Nat.mul_comm (S d)); repeat (rewrite (Nat.mul_comm (S q3)) || rewrite (Nat.mul_comm (S p3)); repeat rewrite <- Nat.mul_assoc); repeat rewrite Nat.mul_sub_distr_r. repeat rewrite (Nat.mul_comm (S d)); repeat rewrite <- Nat.mul_assoc. rewrite <- Heq1; rewrite <- Heq2. rewrite (Nat.mul_comm (S q)); rewrite (Nat.mul_comm (S q')); repeat rewrite Nat.mul_add_distr_r. repeat rewrite Nat.mul_assoc. rewrite Nat.add_comm; rewrite Nat.add_comm; apply Nat.add_sub. auto. simpl in |- *; auto with arith. simpl in |- *; auto with arith. auto. Qed.