proposition: Theorem prime_induction: forall (P: Z -> Prop), P 0 -> P 1 -> (forall p q, prime p -> P q -> P (p * q)) -> forall p, 0 <= p -> P p.
proof: Proof. intros P H H1 H2 p Hp. generalize Hp; pattern p; apply Z_lt_induction; auto; clear p Hp. intros p Rec Hp. case Zle_lt_or_eq with (1 := Hp); clear Hp; intros Hp; subst; auto. case (Zle_lt_or_eq 1 p); auto with zarith; clear Hp; intros Hp; subst; auto. case (prime_dec p); intros H3. rewrite <- (Zmult_1_r p); apply H2; auto. case (Zdivide_div_prime_le_square p); auto. intros q (Hq1, ((q2, Hq2), Hq3)); subst. case (Zmult_interval q q2). rewrite Zmult_comm; apply Z.lt_trans with 1; auto with zarith. apply Z.lt_le_trans with 2; auto with zarith; apply prime_ge_2; auto. intros H4 H5; rewrite Zmult_comm; apply H2; auto. apply Rec. split. 1, 3: auto with zarith. rewrite Zmult_comm; auto. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic