fact: Fixpoint clog2 (p:positive) : nat := match p with xH => 1%nat | xO xH => 2%nat | xO p => S (clog2 p) | xI p => S (clog2 p) end.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)