proposition: Lemma list_nat_spec : forall p a, a <= p -> In a (list_nat p).
proof: Proof. intro p; induction p. intros a Hle; inversion Hle; left; reflexivity. intros a Hle; simpl. case (eq_nat_dec (S p) a). left; assumption. right; apply IHp. inversion Hle. destruct n; symmetry; assumption. assumption. Qed.
imports: Zring Qring Q_can