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