proposition: Theorem divides_dec_aux : forall k n p:nat, n <= k -> divides p n \/ ~divides p n.
proof: Proof. intros k; elim k. - intros n p Hle; left; exists 0; rewrite Nat.mul_comm; simpl; apply (proj1 (Nat.le_0_r _)); auto. - intros k' Hrec n p Hlt; elim (proj1 (Nat.lt_eq_cases n (S k')) Hlt). + auto with arith. + intros Heq; rewrite Heq. case p. * right; intros (q, Heq'). discriminate Heq'. * intros p'; case_eq (Nat.compare (S p') (S k')); intros Htwc. -- assert (H:S p' = S k'). { apply nat_compare_eq; auto. } left; exists 1; rewrite H. auto with arith. -- assert (S p' < S k'). apply nat_compare_Lt_lt; auto. elim (Hrec (minus (S k') (S p')) (S p')). ++ intros (q, Heq'); left; exists (S q). rewrite <- (Nat.sub_add (S p') (S k')), Nat.add_comm. ** rewrite Heq'. repeat rewrite (Nat.mul_comm (S p')). reflexivity. ** auto with arith. ++ intros Hndiv; right; intros Hdiv. apply Hndiv. elim Hdiv. intros q; case q. ** rewrite Nat.mul_comm; simpl; intros; discriminate. ** intros q' Heq'; exists q'. apply Nat.add_cancel_l with (S p'). rewrite Nat.add_comm, Nat.sub_add. { rewrite Heq'. rewrite Nat.add_comm; rewrite mult_n_Sm; reflexivity. } auto with arith. ++ simpl; apply Nat.le_sub_l. -- assert (Hlt': S k' < S p'). { apply nat_compare_Gt_gt; auto. } right; intros Hdiv; elim Hdiv; intros q; case q. ++ rewrite Nat.mul_comm; simpl; intros; discriminate. ++ intros q' Heq'; elim (proj1 (Nat.lt_nge _ _) Hlt'). rewrite Heq'. rewrite Nat.mul_comm; simpl; auto with arith. Qed.
imports: List Arith