proposition: Lemma Zodd_Zeven_min1 : forall x : Z, Zeven.Zodd x -> Zeven.Zeven (x - 1).
proof: Proof. intro x. elim x. simpl in |- *. auto. simple induction p. simpl in |- *. auto. intros p0 H H0. simpl in H0. tauto. simpl in |- *; auto. simple induction p. simpl in |- *; auto. simpl in |- *; auto. auto. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid