proposition: Lemma log2_nonpos n : n<=0 -> log2 n = 0.
proof: Proof. destruct n as [|p|p]; trivial; now destruct 1. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass