proposition: Lemma legal_divide : forall (x : Z) (c : Config), (x > 0)%Z -> Zeven.Zeven x -> legal (Zeven.Zdiv2 x) c -> legal x c.
proof: Proof. intros; apply legal_trans with (c := divide_trans (mkconfig x)). cut (co (mkconfig x) > 0)%Z. intro; cut (Zeven.Zeven (co (mkconfig x))). intro; replace (divide_trans (mkconfig x)) with (next_config (mkconfig x) (divide (mkconfig x) H2 H3)). apply after. apply legal_x_x. auto. auto. auto. auto. Qed.
imports: ZArith Omega