proposition: Lemma mul_mod_distr_l : forall a b c, (c*a) mod (c*b) == c * (a mod b).
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_l. Qed.
imports: NAxioms NSub NDiv