proposition: Lemma list_Q_spec_zero : forall a b d, nat_of_P d <= Z.abs_nat b -> In (Qmake Z0 d) (list_Q a b).
proof: Proof. intros a b d Hle. 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 _) Hle). 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. Qed.
imports: Zring Qring Q_can