Library OSMutexPostPart2_2

Require Import ucert.
Require Import ucert.
Require Import OSQPendPure.
Require Import os_code_defs.
Require Import mathlib.
Require Import OSMutex_common.
Require Import lab.
Require Import gen_lemmas.
Open Scope code_scope.

Lemma tmp: gen_tmp.
  Ltac mew2 := match goal with
                 | |- (if _ then true else false) = true => rewrite ifE
                 | |- (_ <=? _ = true) => apply Zle_imp_le_bool
                 | |- (_ <= _ ) => apply Zle_bool_imp_le
               end.

Lemma tmp2: gen_tmp2.