proposition: Lemma odd_pred2n: forall n : nat, Nat.Odd_alt n -> {p : nat | n = pred (Nat.double p)}.
proof: Proof. intros n H_odd; apply Nat.Odd_alt_Odd in H_odd; rewrite (Nat.Odd_double _ H_odd); exists (S (Nat.div2 n)); generalize (Nat.div2 n); clear n H_odd; intros n; unfold Nat.double; rewrite Nat.add_succ_r; reflexivity. Defined.
imports: Coq(ZArith) Coq(Lia)