proposition: Lemma pred_double_spec p : pred_double p = pred (p~0).
proof: Proof. reflexivity. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef