proposition: Lemma hoare_while : forall b (P Q: assn) c, |- {{s | P s /\ bval s b}} c {{P}} -> (forall s, P s /\ negb (bval s b) -> Q s) -> |- {{P}} (While b Do c) {{Q}}.
proof: Proof. sauto use: lem_hoare_weaken_post unfold: entails. Qed.
imports: Hammer(Tactics Reflect) String Arith Lia Relations