proposition: Lemma eq_mul_1_nonneg : forall n m, 0<=n -> n*m == 1 -> n==1 /\ m==1.
proof: Proof. intros n m Hn H. le_elim Hn. - destruct (lt_ge_cases m 0) as [Hm|Hm]. + generalize (mul_pos_neg n m Hn Hm). order'. + le_elim Hm. * apply le_succ_l in Hn. rewrite <- one_succ in Hn. le_elim Hn. -- generalize (lt_1_mul_pos n m Hn Hm). order. -- rewrite <- Hn, mul_1_l in H. now split. * rewrite <- Hm, mul_0_r in H. order'. - rewrite <- Hn, mul_0_l in H. order'. Qed.
imports: NZAxioms NZMulOrder