proposition: Lemma decomp : forall s : state, s = mkstate (state_n s) (state_p s) (state_b s).
proof: Proof. simple induction s; simpl in |- *; 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