proposition: Lemma final_inv : forall (n p : nat) (b : bool), final (mkstate n p b) -> n = one.
proof: Proof. intros. inversion_clear H; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Wf_nat euclid Le_lt_compl Euclid shift Compare_dec imperative while two_power log2_spec