proposition: Lemma div_exact (a b : nat) : a = b * (a / b) <-> a mod b = 0.
proof: Proof. rewrite [X in X = _](Nat.div_mod_eq a b). lia. 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