proposition: Lemma mm_state_ub y : mm2_reaches c0 y -> fst y < state_bound.
proof: Proof. move=> /(@clos_rt_rtn1 mm2_state). elim. - rewrite /state_bound /=. lia. - move=> > [?] [/mm2_instr_at_state_bound + H] _. case: H => > /=; lia. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun