proposition: Lemma mod_divides : forall a b, (a mod b == 0 <-> exists c, a == b*c).
proof: Proof. intros a b. destruct (eq_decidable b 0) as [Hb|Hb]. - split. + intros Hab. exists 0. revert Hab. rewrite Hb. now nzsimpl. + intros [c Hc]. revert Hc. rewrite Hb. now nzsimpl. - now apply mod_divides. Qed.
imports: NAxioms NSub NDiv