proposition: Lemma divide_antisym_abs : forall n m, (n | m) -> (m | n) -> abs n == abs m.
proof: Proof. intros. apply divide_antisym_nonneg; try apply abs_nonneg. - now apply divide_abs_l, divide_abs_r. - now apply divide_abs_l, divide_abs_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZGcd