proposition: Theorem div2_spec: forall n, ({x : nat | 2 * x = n}) + ({x : nat | 2 * x + 1 = n}).
proof: Proof. intros n; induction n as [| | n IHn] using div2_rec. - left; now exists 0. - right; now exists 0. - destruct IHn as [[x Heq]|[x Heq]]. + left; exists (S x); rewrite <- Heq; ring. + right; exists (S x); rewrite <- Heq; ring. Qed.
imports: Arith ArithRing Wf_nat fib_ind fib_positive Lia