proposition: Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m].
proof: Proof. intros n m. split. - intros (p,H). exists [p]. revert H; now zify. - intros (z,H). exists (of_N (Z.abs_N z)). zify. rewrite N2Z.inj_abs_N. rewrite <- (Z.abs_eq [m]), <- (Z.abs_eq [n]) by apply spec_pos. now rewrite H, Z.abs_mul. Qed.
imports: ZArith OrdersFacts Nnat NAxioms NSig Lia