proposition: Lemma get_representative : forall ab, {v | In v representatives /\ RZ v ab}.
proof: Proof. move=> [[|a] [|b]]; rewrite /representatives /RZ. - exists (0, 0) => /=. split; [tauto|lia]. - exists (0, 1) => /=. split; [tauto|lia]. - exists (1, 0) => /=. split; [tauto|lia]. - exists (1, 1) => /=. split; [tauto|lia]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun