proposition: Lemma size_gt n : n < 2^(size n).
proof: Proof. destruct n. - reflexivity. - simpl. apply Pos.size_gt. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties