proposition: Lemma mod_mul_r : forall a b c, a mod (b*c) == a mod b + b*((a/b) mod c).
proof: Proof. intros a b c. destruct (eq_decidable b 0) as [->|Hb]. - now nzsimpl. - destruct (eq_decidable c 0) as [->|Hc]. + nzsimpl. rewrite add_comm. apply div_mod. + now apply mod_mul_r. Qed.
imports: NAxioms NSub NDiv