proposition: Corollary mod_add_mod : forall a b n c, (b <> 0)%Z -> (exists k, b = (k * c)%Z) -> ((a mod b + n) mod c = (a + n) mod c)%Z.
proof: Proof. intros a b n c. rewrite <-(Z.mul_1_r (a mod b)). rewrite <-(Z.mul_1_r a) at 2. apply mod_mul_add_mod. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)