proposition: Lemma list_Q_spec : forall (a b : Z_as_CRing) q, a [#] [0] -> b [#] [0] -> Zdivides (Q_can_num q) a -> Zdivides (Z.abs_nat (Q_can_den_pos_val q)) b -> In (Q_can q) (list_Q a b).
proof: Proof. intros a b q Hapa Hapb Ha Hb. destruct q as [qn qd]. destruct qn. apply list_Q_spec_zero. revert Hb; generalize (Q_can_den_pos_val (0#qd)%Q). intros p Hdiv. assert (nat_of_P p = Z.abs_nat p). reflexivity. rewrite H; apply div_imp_leq. assumption. rewrite inj_Zabs_nat in Hdiv. apply Zdivides_abs_intro_lft; assumption. apply list_Q_spec_pos. apply div_imp_leq; assumption. apply div_imp_leq. assumption. apply Zdivides_abs_intro_lft. rewrite <- inj_Zabs_nat. assumption. apply list_Q_spec_neg. apply div_imp_leq; assumption. apply div_imp_leq. assumption. apply Zdivides_abs_intro_lft. rewrite <- inj_Zabs_nat. assumption. Qed.
imports: Zring Qring Q_can