proposition: Lemma log2_nonpos n : n<=0 -> log2 n = 0.
proof: Proof. destruct n; intros Hn. - reflexivity. - now destruct Hn. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties