proposition: Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1.
proof: Proof. assert (F := lt_m1_0). intro n; zero_pos_neg n. - intros m. nzsimpl. now left. - intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn. le_elim Hn; split; intros m H. + destruct (lt_1_mul_l n m) as [|[|]]; order'. + rewrite mul_opp_l, eq_opp_l in H. destruct (lt_1_mul_l n m) as [|[|]]; order'. + now left. + intros; right. now f_equiv. Qed.
imports: ZAddOrder