proposition: Lemma two_power_monoR : forall n p : nat, two_power n < two_power p -> n < p.
proof: Proof. intros. apply not_le_lt. unfold not in |- *; intro. elim (lt_not_le (two_power n) (two_power p) H). case (le_lt_or_eq p n H0); intro. apply lt_le_weak. apply two_power_mono; auto with arith. auto with arith. rewrite H1; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Le_lt_compl