Library OSMutexPostPart30

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

Lemma post3 : gen_post3.
    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 post5 :gen_post5.

Lemma post1´ :gen_post1´.

Lemma post3´ : gen_post3´.

Lemma post5´ :gen_post5´.

Theorem MutexPostPart3133:gen_MutexPostPart3133.
Require Import OSQPostPure.