proposition: Lemma mult_ppq_p0q1 : forall p q : nat, p = p * q -> p = 0 \/ q = 1.
proof: Proof. intro p. case p. left. reflexivity. intro p1. right. apply simpl_eq_mult_l with (S p1). apply lt_O_Sn. rewrite <- H. rewrite <- mult_n_Sm. rewrite <- mult_n_O. simpl in |- *. reflexivity. Qed.
imports: ZArith EqNat