proposition: Lemma lt_multpred_pp : forall p : nat, p > 1 -> pred p * pred p < p * p.
proof: Proof. intro. case p. intro. elim (lt_n_O 1). assumption. intro p1. case p1. intro. elim (lt_irrefl 1). assumption. intro p2. intros. apply lt_lt_mult. simpl in |- *. apply lt_n_Sn. simpl in |- *. apply lt_n_Sn. Qed.
imports: ZArith EqNat