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_Z z). now zify. Qed.
imports: Bool ZArith OrdersFacts Nnat ZAxioms ZSig Lia