proposition: Theorem omod_divide : ∀ a b : nat, b ≠ 0%nat → a omod b = 0%nat ↔ (b | a).
proof: Proof. intros * Hbz. unfold omodulo. destruct (Nat.eq_dec b 0) as [H| H]; [ easy | ]. now apply Nat.mod_divide. Qed.
imports: Utf8 QArith NPeano Sorted Psatz