proposition: Theorem square_not_prime: forall a, ~ prime (a * a).
proof: Proof. intros a Ha. rewrite <- (Z.abs_square a) in Ha. assert (H:=Z.abs_nonneg a). set (b:=Z.abs a) in *; clearbody b; clear a; rename b into a. rewrite <- prime_alt in Ha; destruct Ha as (Ha,Ha'). assert (H' : 1 < a) by now apply (Z.square_lt_simpl_nonneg 1). apply (Ha' a). + split; trivial. rewrite <- (Z.mul_1_l a) at 1. apply Z.mul_lt_mono_pos_r; auto. apply Z.lt_trans with (2 := H'); red; auto. + exists a; auto. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat