proposition: Lemma divide_antisym_nonneg : forall n m, 0<=n -> 0<=m -> (n | m) -> (m | n) -> n == m.
proof: Proof. intros n m Hn Hm (q,Hq) (r,Hr). le_elim Hn. - destruct (lt_ge_cases q 0) as [Hq'|Hq']. + generalize (mul_neg_pos q n Hq' Hn). order. + rewrite Hq, mul_assoc in Hr. symmetry in Hr. apply mul_id_l in Hr; [|order]. destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial. now rewrite H, mul_1_l in Hq. - rewrite <- Hn, mul_0_r in Hq. now rewrite <- Hn. Qed.
imports: NZAxioms NZMulOrder