proposition: Lemma decreasing_measure : forall (c : Config) (t : transition c), (co c > co (next_config c t))%Z.
proof: Proof. simple induction t. simpl in |- *; intros. omega. simpl in |- *. intros. apply x_gt_Zdiv2. auto. auto. Qed.
imports: ZArith Omega