proposition: Lemma candidate_app l1 l2 : candidate_list (l1 ++ l2) = candidate_list l1 ++ candidate_list l2.
proof: Proof. revert l2; elim l1; unfold candidate_list; clear l1. - simpl; auto. - intros a l1 Hrec l2; rewrite fold_right_cons. rewrite app_ass, <- Hrec; auto. Qed.
imports: ZArith List