proposition: Lemma counter_remains_positive_or_null : forall (x : Z) (c : Config), (x >= 0)%Z -> legal x c -> (co c >= 0)%Z.
proof: Proof. intros. elim H0. simpl in |- *. auto. simple induction t. simpl in |- *. intros. omega. simpl in |- *. intros. apply Zdiv2_positive. auto. auto. Qed.
imports: ZArith Omega