proposition: Lemma not_final : forall (n p : nat) (b : bool), invar (mkstate n p b) -> ~ final (mkstate n p b) -> one < n.
proof: Proof. intros. case (le_or_lt n one); [ intro | auto with arith ]. cut (0 < n); [ intro | apply invar_inv3 with p b; auto with arith ]. case (enum1 n). unfold two in |- *; auto with arith. intro; absurd (0 < n); auto with arith. rewrite H3; auto with arith. intro; absurd (final (mkstate n p b)); [ auto with arith | idtac ]. rewrite H3; split; 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