proposition: Lemma reaches_neq_incl {x y} : reaches x y -> x <> y -> reaches_plus x y.
proof: Proof. move=> /clos_rt_rtn1_iff []; [done|]. move=> ??? /clos_rt_rtn1_iff? _. by apply: clos_rt_t; [|apply: t_step]; eassumption. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun