proposition: Lemma size_log2 n : n<>0 -> size n = succ (log2 n).
proof: Proof. destruct n as [|[n|n| ]]; trivial. now destruct 1. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties