proposition: Lemma divide n m : (Z.of_nat n | Z.of_nat m) ↔ (n | m)%nat.
proof: Proof. split. - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i). lia. - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)