Library hydras.Prelude.Exp2

From Coq Require Import Arith Lia.

Fixpoint exp2 (n:nat) : nat :=
  match n with
    0 ⇒ 1
  | S i ⇒ 2 × exp2 i
  end.

Lemma exp2_positive : ∀ i, 0 < exp2 i.

Lemma exp2_not_zero i : exp2 i ≠ 0.

Lemma exp2_gt_id : ∀ n, n < exp2 n.

Lemma exp2S : ∀ n, exp2 (S n) = 2 × exp2 n.