proposition: Lemma two_power_le : forall n p : nat, n <= p -> two_power n <= two_power p.
proof: Proof. intros n p H; case (le_lt_or_eq _ _ H); intro H1. apply lt_le_weak; apply two_power_mono; auto with arith. rewrite H1; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Le_lt_compl