proposition: Lemma mult_pq1_p1q1 : forall p q : nat, p * q = 1 -> p = 1 /\ q = 1.
proof: Proof. intro p. case p. simpl in |- *. intros. discriminate H. intro p1. case p1. simpl in |- *. intro q. rewrite <- plus_n_O. split. reflexivity. assumption. intro p2. intro q. case q. rewrite <- mult_n_O. intro. discriminate H. intro q1. case q1. rewrite <- mult_n_Sm. rewrite <- mult_n_O. simpl in |- *. intro. discriminate H. intro q2. simpl in |- *. intro. discriminate H. Qed.
imports: ZArith EqNat