proposition: Lemma mult_SO : forall x y : nat, x * y = 1 -> x = 1.
proof: Proof. intros x; case x; simpl in |- *; auto. intros x' y; case y; simpl in |- *; auto. rewrite Nat.mul_comm; intros; discriminate. intros n H'; case (mult_eqO x' (S n)). apply plus_eqO with (y := n). rewrite Nat.add_comm; apply eq_add_S; auto. intros H'0; rewrite H'0; auto. intros; discriminate. Qed.
imports: Coq(Arith ArithRing)