proposition: Lemma mul_mod (a b n : nat) : (a * b) mod n = (a mod n * (b mod n)) mod n.
proof: Proof. move: n => [|n]. - reflexivity. - apply: Nat2Z.inj. rewrite !(Nat2Z.inj_mod, Nat2Z.inj_mul). by apply: Z.mul_mod. Qed.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun