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