proposition: Corollary cmod_mul_add_mod : forall a b m n c, (b <> 0)%Z -> (exists k, b = (k * c)%Z) -> ((a cmod b * m + n) mod c = (a * m + n) mod c)%Z.
proof: Proof. intros a b m n c. unfold Zcmod. rewrite Z.mul_sub_distr_r. replace (a * m)%Z with ((a + Z.quot b 2) * m - (Z.quot b 2) * m)%Z by ring. unfold Z.sub. rewrite <-2Z.add_assoc. apply mod_mul_add_mod. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)