proposition: Lemma zero_lt_pow : forall a : nat, 0 < two_power a.
proof: Proof. simple induction a; simpl in |- *. auto with arith. intros. apply lt_plus_trans; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Le_lt_compl