proposition: Lemma two_power_mono : forall n p : nat, n < p -> two_power n < two_power p.
proof: Proof. simple induction 1. intros; apply two_power_S_lt; auto with arith. intros. apply lt_trans with (two_power m); auto with arith. apply two_power_S_lt; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Le_lt_compl