proposition: Lemma add_mul_mod_distr_l : forall a b c d, b~=0 -> 0<=d<c -> (c*a+d) mod (c*b) == c*(a mod b)+d.
proof: Proof. intros a b c d Hb ?. apply add_mul_mod_distr_l. - apply le_0_l. - assert (H'b := le_0_l b). order. - assumption. Qed.
imports: NAxioms NSub NZDiv