proposition: Lemma size_le n : 2^(size n) <= succ_double n.
proof: Proof. destruct n as [|p]. - discriminate. - simpl. change (2^Pos.size p <= Pos.succ (p~0))%positive. apply Pos.lt_le_incl, Pos.lt_succ_r, Pos.size_le. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties