proposition: Lemma log2_unicity : forall n p z : nat, two_power n < z -> z < two_power (S n) -> two_power p < z -> z < two_power (S p) -> n = p.
proof: Proof. intros. case (le_or_lt n p); intros. case (le_lt_or_eq n p H3); intros. absurd (z < z). auto with arith. apply lt_trans with (two_power (S n)). auto with arith. apply le_lt_trans with (two_power p). apply two_power_le; auto with arith. auto with arith. auto with arith. absurd (z < z). auto with arith. apply lt_trans with (two_power (S p)). auto with arith. apply le_lt_trans with (two_power n). apply two_power_le; auto with arith. auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Le_lt_compl