proposition: Theorem div2_rec: forall (P : nat -> Set), P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall (n : nat), P n.
proof: Proof. intros P H0 H1 Hrec n; assert (P n * P (S n))%type. - elim n; intuition. - intuition. Qed.
imports: Arith ArithRing Wf_nat fib_ind fib_positive Lia