proposition: Lemma size_gt p : p < 2^(size p).
proof: Proof. induction p as [p IHp|p IHp|]; simpl; try rewrite pow_succ_r; try easy. apply le_succ_l in IHp. now apply le_succ_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef