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 Hrec] using div2_rect. - left; now exists 0. - right; now exists 0. - destruct Hrec as [[x Heq]|[x Heq]]. + left; exists (S x); rewrite <- Heq; ring. + right; exists (S x); rewrite <- Heq; ring. Qed.
imports: Arith ArithRing Lia fib_ind