proposition: Lemma list_Q_spec_pos : forall a b c d, Z.abs_nat c <= Z.abs_nat a -> Z.abs_nat (Zpos d) <= Z.abs_nat b -> In (Qmake c d) (list_Q a b).
proof: Proof. intros a b c d Hca Hdb. case (Qeq_dec (c#d)%Q [0]). unfold Qeq; simpl; rewrite Zmult_1_r. intro Heq; rewrite Heq. clear c Hca Heq. unfold list_Q. rewrite -> in_flat_map. exists (0, pred (nat_of_P d)). split. apply list_nat_prod_spec. apply Nat.le_0_l. apply (Nat.le_trans _ _ _ (Nat.le_pred_l _) Hdb). left. f_equal. destruct (ZL4 d). rewrite H. simpl. rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H. apply nat_of_P_inj; symmetry; assumption. unfold list_Q. intro H. rewrite -> in_flat_map. exists (Z.abs_nat c, Z.abs_nat d). split. apply list_nat_prod_spec; assumption. simpl. case (ZL4 d). intros d' Hd'. unfold Z.abs_nat at 1 in Hdb. rewrite Hd'. rewrite Hd' in Hdb. case_eq (Z.abs_nat c). intro Heq. destruct H. destruct c. reflexivity. simpl in Heq; destruct (ZL4 p); rewrite Heq in H; discriminate. simpl in Heq; destruct (ZL4 p); rewrite Heq in H; discriminate. intros. destruct c as [|c|c]. discriminate. constructor 1. unfold Qeq; simpl. assert (c = P_of_succ_nat n). rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H0. simpl in H. apply nat_of_P_inj; assumption. rewrite H1. cut (P_of_succ_nat d' = d). intro H2; rewrite H2; reflexivity. apply nat_of_P_inj. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. symmetry; assumption. constructor 2. constructor 1. unfold Qeq; simpl. assert (c = P_of_succ_nat n). rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H0. simpl in H. apply nat_of_P_inj; assumption. rewrite H1. cut (P_of_succ_nat d' = d). intro H2; rewrite H2; reflexivity. apply nat_of_P_inj. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. symmetry; assumption. Qed.
imports: Zring Qring Q_can