proposition: Lemma two_power_S : forall n : nat, two_power (S n) = two_power n * two.
proof: Proof. intros; unfold two_power at 1 in |- *; rewrite mult_comm; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Le_lt_compl