proposition: Lemma legal_decrement : forall (x : Z) (c : Config), (x > 0)%Z -> Zeven.Zodd x -> legal (x - 1) c -> legal x c.
proof: Proof. intros; apply legal_trans with (c := decrement_trans (mkconfig x)). cut (co (mkconfig x) > 0)%Z. intro; cut (Zeven.Zodd (co (mkconfig x))). intro; replace (decrement_trans (mkconfig x)) with (next_config (mkconfig x) (decrement (mkconfig x) H2 H3)). apply after. apply legal_x_x. auto. auto. simpl in |- *. auto. auto. Qed.
imports: ZArith Omega