proposition: Lemma mult_eq_Sn : forall a b : nat, 0 < b -> a * b = b -> a = 1.
proof: Proof. intros a b; case b; simpl in |- *; auto. intros H; Contradict H; auto with arith. case a; simpl in |- *; auto. intros; discriminate. intros b' a' H' H'1; case (mult_eqO b' (S a')); auto. apply Nat.add_cancel_l with (p := S a'); simpl in |- *; rewrite <- plus_n_O; auto. intros H'0; Contradict H'0; auto; rewrite H'0; auto with arith. Qed.
imports: Coq(Arith ArithRing)