proposition: Lemma pred_double_xO_discr p : pred_double p <> p~0.
proof: Proof. now destruct p. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef