Library OSMutexPostPart3

Require Import ucert.
Require Import ucert.
Require Import OSMutexPostPart30.
Require Import OSMutexPostPart3_3.
Require Import OSMutexPostPure.
Require Import os_code_defs.
Require Import mathlib.
Require Import OSMutex_common.
Require Import lab.
Require Import gen_lemmas.
Open Scope code_scope.

Lemma MutexPostPart3 : gen_MutexPostPart3.
    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.
   Require Import OSTimeDlyPure.