proposition: Lemma invar_inv3 : forall (n p : nat) (b : bool), invar (mkstate n p b) -> 0 < n.
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