proposition: Lemma two_power_S_lt : forall n : nat, two_power n < two_power (S n).
proof: Proof. intro; rewrite two_power_S. rewrite mult_comm; apply mult_p_lt_qp; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Le_lt_compl