proposition: Lemma mod_mul_add_mod : forall a b m n c, (b <> 0)%Z -> (exists k, b = (k * c)%Z) -> ((a mod b * m + n) mod c = (a * m + n) mod c)%Z.
proof: Proof. intros a b m n c Ib_neq_0 [k Heq_b]. generalize (Zdiv.Z_div_mod_eq_full a b). intros Haux. rewrite Z.add_comm in Haux. apply Z.sub_move_r in Haux. rewrite <-Haux. clear Haux. rewrite Heq_b at 1. rewrite Z.mul_sub_distr_r, <-Z.add_sub_swap. unfold Z.sub. rewrite (Z.mul_comm k c), <-!Z.mul_assoc, (Z.mul_comm c), <-Z.mul_opp_l. apply Z.mod_add. lia. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)