proposition: Lemma add_mul_mod_distr_r : forall a b c d, d<c -> (a*c+d) mod (b*c) == (a mod b)*c+d.
proof: Proof. intros a b c d ?. destruct (eq_decidable b 0) as [->|Hb]. - now nzsimpl. - apply add_mul_mod_distr_r; intuition auto using le_0_l. Qed.
imports: NAxioms NSub NDiv